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
Iris
c
Commits
0713b216
Commit
0713b216
authored
Jun 07, 2018
by
Dan Frumin
Browse files
Hacking x 2
parent
612d5dd0
Changes
4
Hide whitespace changes
Inline
Side-by-side
_CoqProject
View file @
0713b216
...
...
@@ -9,9 +9,12 @@ theories/c_translation/monad.v
theories/c_translation/proofmode.v
theories/c_translation/translation.v
theories/c_translation/derived.v
theories/heap_lang_vcgen/dval.v
theories/heap_lang_vcgen/vcgen.v
theories/heap_lang_vcgen/test.v
theories/vcgen/dval.v
theories/vcgen/vcgen.v
# theories/vcgen/test.v
# theories/heap_lang_vcgen/dval.v
# theories/heap_lang_vcgen/vcgen.v
# theories/heap_lang_vcgen/test.v
theories/tests/test1.v
theories/tests/test2.v
theories/tests/fact.v
...
...
theories/heap_lang_vcgen/vcgen.v
View file @
0713b216
...
...
@@ -242,8 +242,7 @@ Section vcg.
case_bool_decide
;
first
done
.
naive_solver
.
Qed
.
Fixpoint
optimize
(
s
:
list
(
nat
*
dval
))
(
Φ
:
wp_expr
)
:
wp_expr
:
=
exhale_list
s
Φ
.
(*
Fixpoint
optimize
(
s
:
list
(
nat
*
dval
))
(
Φ
:
wp_expr
)
:
wp_expr
:
=
match
Φ
with
|
Base
Φ
1
=>
exhale_list
s
Φ
|
Inhale
dl
Φ
1
=>
...
...
@@ -268,8 +267,10 @@ Section vcg.
IsLoc
dv
(
λ
v
,
optimize
s
(
Φ
1
v
))
|
_
=>
Base
False
end
|
Par
P1
P2
P3
=>
Par
(
λ
Ψ
1
,
optimize
s
(
P1
Ψ
1
))
(
λ
Ψ
2
,
optimize
s
(
P2
Ψ
2
))
(
λ
v1
v2
,
optimize
s
(
P3
v1
v2
))
end
.
*)
Lemma
vcg_opt_list_sound'
(
E
:
list
loc
)
(
pl
:
list
(
nat
*
dval
))
(
Φ
:
wp_expr
)
:
wp_interp
E
(
optimize
pl
Φ
)
-
∗
...
...
@@ -422,4 +423,4 @@ Section vcg.
iIntros
(
v
)
"H"
.
by
iDestruct
"H"
as
(
dv
)
"[-> H2]"
.
Qed
.
End
vcg
.
\ No newline at end of file
End
vcg
.
theories/vcgen/dval.v
0 → 100644
View file @
0713b216
From
iris
.
heap_lang
Require
Export
proofmode
notation
.
From
iris
.
bi
Require
Import
big_op
.
Inductive
dloc
:
=
|
dLoc
:
nat
→
dloc
|
dLocUnknown
:
loc
→
dloc
.
Global
Instance
dloc_decision
:
EqDecision
dloc
.
Proof
.
solve_decision
.
Defined
.
Inductive
dbase_lit
:
Type
:
=
|
dLitInt
:
Z
→
dbase_lit
|
dLitBool
:
bool
→
dbase_lit
|
dLitUnit
:
dbase_lit
|
dLitLoc
:
dloc
→
dbase_lit
|
dLitUnknown
:
base_lit
→
dbase_lit
.
Global
Instance
dlit_decision
:
EqDecision
dbase_lit
.
Proof
.
solve_decision
.
Defined
.
Inductive
dval
:
Type
:
=
|
dLitV
:
dbase_lit
→
dval
|
dValUnknown
:
val
→
dval
.
Inductive
doption
(
A
:
Type
)
:
Type
:
=
|
dNone
:
doption
A
|
dSome
:
A
→
doption
A
|
dUnknown
:
option
A
→
doption
A
.
Arguments
dNone
{
_
}.
Arguments
dSome
{
_
}
_
.
Arguments
dUnknown
{
_
}
_
.
Global
Instance
doption_fmap
:
FMap
doption
:
=
λ
A
B
f
m
,
match
m
with
|
dNone
=>
dNone
|
dSome
x
=>
dSome
(
f
x
)
|
dUnknown
o
=>
dUnknown
(
f
<$>
o
)
end
.
Definition
dloc_interp
(
E
:
list
loc
)
(
dl
:
dloc
)
:
loc
:
=
match
dl
with
|
dLoc
i
=>
from_option
id
inhabitant
(
E
!!
i
)
|
dLocUnknown
l
=>
l
end
.
Definition
dbase_lit_interp
(
E
:
list
loc
)
(
l
:
dbase_lit
)
:
base_lit
:
=
match
l
with
|
dLitInt
x
=>
LitInt
x
|
dLitBool
b
=>
LitBool
b
|
dLitUnit
=>
LitUnit
|
dLitLoc
dl
=>
LitLoc
(
dloc_interp
E
dl
)
|
dLitUnknown
l
=>
l
end
.
Definition
dval_interp
(
E
:
list
loc
)
(
v
:
dval
)
:
val
:
=
match
v
with
|
dLitV
l
=>
LitV
(
dbase_lit_interp
E
l
)
|
dValUnknown
v
=>
v
end
.
Fixpoint
doption_interp
{
A
}
(
mx
:
doption
A
)
:
option
A
:
=
match
mx
with
|
dNone
=>
None
|
dSome
x
=>
Some
x
|
dUnknown
mx
=>
mx
end
.
Definition
dbin_op_eval_int
(
op
:
bin_op
)
(
n1
n2
:
Z
)
:
dbase_lit
:
=
match
op
with
|
PlusOp
=>
dLitInt
(
n1
+
n2
)
|
MinusOp
=>
dLitInt
(
n1
-
n2
)
|
MultOp
=>
dLitInt
(
n1
*
n2
)
|
QuotOp
=>
dLitInt
(
n1
`
quot
`
n2
)
|
RemOp
=>
dLitInt
(
n1
`
rem
`
n2
)
|
AndOp
=>
dLitInt
(
Z
.
land
n1
n2
)
|
OrOp
=>
dLitInt
(
Z
.
lor
n1
n2
)
|
XorOp
=>
dLitInt
(
Z
.
lxor
n1
n2
)
|
ShiftLOp
=>
dLitInt
(
n1
≪
n2
)
|
ShiftROp
=>
dLitInt
(
n1
≫
n2
)
|
LeOp
=>
dLitBool
(
bool_decide
(
n1
≤
n2
))
|
LtOp
=>
dLitBool
(
bool_decide
(
n1
<
n2
))
|
EqOp
=>
dLitBool
(
bool_decide
(
n1
=
n2
))
end
.
Lemma
dbin_op_eval_int_correct
E
op
n1
n2
:
bin_op_eval_int
op
n1
n2
=
dbase_lit_interp
E
(
dbin_op_eval_int
op
n1
n2
).
Proof
.
by
destruct
op
.
Qed
.
Definition
dbin_op_eval_bool
(
op
:
bin_op
)
(
b1
b2
:
bool
)
:
doption
dbase_lit
:
=
match
op
with
|
PlusOp
|
MinusOp
|
MultOp
|
QuotOp
|
RemOp
=>
dNone
(* Arithmetic *)
|
AndOp
=>
dSome
(
dLitBool
(
b1
&&
b2
))
|
OrOp
=>
dSome
(
dLitBool
(
b1
||
b2
))
|
XorOp
=>
dSome
(
dLitBool
(
xorb
b1
b2
))
|
ShiftLOp
|
ShiftROp
=>
dNone
(* Shifts *)
|
LeOp
|
LtOp
=>
dNone
(* InEquality *)
|
EqOp
=>
dSome
(
dLitBool
(
bool_decide
(
b1
=
b2
)))
end
.
Lemma
dbin_op_eval_bool_correct
E
op
b1
b2
w
:
dbin_op_eval_bool
op
b1
b2
=
dSome
w
→
bin_op_eval_bool
op
b1
b2
=
Some
(
dbase_lit_interp
E
w
).
Proof
.
destruct
op
;
simpl
;
try
by
inversion
1
.
Qed
.
Definition
dbin_op_eval
(
E
:
list
loc
)
(
op
:
bin_op
)
(
dv1
dv2
:
dval
)
:
doption
dval
:
=
match
dv1
,
dv2
with
|
dValUnknown
_
,
_
|
_
,
dValUnknown
_
=>
dUnknown
(
dValUnknown
<$>
bin_op_eval
op
(
dval_interp
E
dv1
)
(
dval_interp
E
dv2
))
|
dLitV
l1
,
dLitV
l2
=>
if
decide
(
op
=
EqOp
)
then
dSome
$
dLitV
$
dLitBool
$
bool_decide
(
dbase_lit_interp
E
l1
=
dbase_lit_interp
E
l2
)
else
match
l1
,
l2
with
|
(
dLitInt
n1
),
(
dLitInt
n2
)
=>
dSome
$
dLitV
$
dbin_op_eval_int
op
n1
n2
|
(
dLitBool
b1
),
(
dLitBool
b2
)
=>
dLitV
<$>
dbin_op_eval_bool
op
b1
b2
|
dLitUnknown
_
,
_
|
_
,
dLitUnknown
_
=>
dUnknown
(
dValUnknown
<$>
bin_op_eval
op
(
dval_interp
E
dv1
)
(
dval_interp
E
dv2
))
|
_
,
_
=>
dNone
end
end
.
Lemma
dbin_op_eval_correct
E
op
dv1
dv2
w
:
doption_interp
(
dbin_op_eval
E
op
dv1
dv2
)
=
Some
w
→
bin_op_eval
op
(
dval_interp
E
dv1
)
(
dval_interp
E
dv2
)
=
Some
(
dval_interp
E
w
).
Proof
.
destruct
dv1
as
[
dl1
|
v1
].
-
destruct
dv2
as
[
dl2
|
v2
].
+
unfold
bin_op_eval
.
simpl
.
case_decide
;
simplify_eq
/=.
{
inversion
1
.
rewrite
/
bin_op_eval
/=.
f_equal
.
simplify_eq
/=.
do
2
case_bool_decide
;
simplify_eq
/=
;
eauto
.
destruct
H0
.
done
.
}
{
rewrite
/
bin_op_eval
;
intros
;
destruct
dl1
,
dl2
;
rewrite
/
bin_op_eval_int
/
bin_op_eval_bool
;
simplify_eq
/=
;
f_equal
;
try
(
destruct
op
;
done
)
;
simpl
.
-
rewrite
/
bin_op_eval
in
H0
;
case_decide
;
first
done
.
destruct
b
;
simplify_eq
/=
;
f_equal
.
-
destruct
op
;
simplify_eq
/=
;
try
done
.
-
case_decide
;
first
done
.
destruct
b0
;
simplify_eq
/=
;
f_equal
.
destruct
op
;
simplify_eq
/=
;
try
done
.
-
case_decide
;
first
done
.
destruct
b
;
simplify_eq
/=
;
f_equal
.
-
case_decide
;
first
done
;
destruct
b
;
simplify_eq
/=
;
f_equal
;
destruct
op
;
simplify_eq
/=
;
try
done
.
-
case_decide
;
first
done
;
destruct
b
;
simplify_eq
/=
;
f_equal
.
-
case_decide
;
first
done
;
destruct
b
;
simplify_eq
/=
;
f_equal
.
-
case_decide
;
first
done
;
destruct
b
,
b0
;
simplify_eq
/=
;
f_equal
.
destruct
op
;
simplify_eq
/=
;
try
done
.
}
+
simpl
;
destruct
(
bin_op_eval
op
#(
dbase_lit_interp
E
dl1
)
v2
)
;
try
by
inversion
1
.
-
simpl
;
destruct
(
bin_op_eval
op
v1
(
dval_interp
E
dv2
))
;
try
by
inversion
1
.
Qed
.
(** ** LocLookup *)
Class
LocLookup
(
E
:
list
loc
)
(
l
:
loc
)
(
i
:
nat
)
:
=
loc_lookup
:
E
!!
i
=
Some
l
.
Global
Instance
loc_lookup_here
l
E
:
LocLookup
(
l
::
E
)
l
0
.
Proof
.
done
.
Qed
.
Global
Instance
loc_lookup_there
l
l'
E
i
:
LocLookup
E
l
i
→
LocLookup
(
l'
::
E
)
l
(
S
i
).
Proof
.
done
.
Qed
.
(** ** BaseLitQuote *)
Class
BaseLitQuote
(
E
:
list
loc
)
(
l
:
base_lit
)
(
dl
:
dbase_lit
)
:
=
base_lit_quote
:
l
=
dbase_lit_interp
E
dl
.
(** BaseLitQuote for locs *)
Global
Instance
base_lit_quote_loc
E
l
i
:
LocLookup
E
l
i
→
BaseLitQuote
E
(
LitLoc
l
)
(
dLitLoc
(
dLoc
i
))
|
1
.
Proof
.
by
rewrite
/
LocLookup
/
BaseLitQuote
/=
=>
->.
Qed
.
Global
Instance
base_lit_quote_loc_unknown
E
l
:
BaseLitQuote
E
(
LitLoc
l
)
(
dLitLoc
(
dLocUnknown
l
))
|
10
.
Proof
.
done
.
Qed
.
(** BaseLitQuote for constants *)
Global
Instance
base_lit_quote_int
E
i
:
BaseLitQuote
E
(
LitInt
i
)
(
dLitInt
i
).
Proof
.
by
rewrite
/
BaseLitQuote
/=.
Qed
.
Global
Instance
base_lit_quote_default
E
l
:
BaseLitQuote
E
l
(
dLitUnknown
l
)
|
1000
.
Proof
.
done
.
Qed
.
Class
IntoDVal
(
E
:
list
loc
)
(
e
:
expr
)
(
dv
:
dval
)
:
=
into_dval
:
e
=
of_val
(
dval_interp
E
dv
).
Global
Instance
into_dval_loc
E
l
dl
:
BaseLitQuote
E
l
dl
→
IntoDVal
E
(
Lit
l
)
(
dLitV
dl
).
Proof
.
by
rewrite
/
BaseLitQuote
/
IntoDVal
=>
->.
Qed
.
Global
Instance
into_dval_default
E
e
v
:
IntoVal
e
v
→
IntoDVal
E
e
(
dValUnknown
v
)
|
1000
.
Proof
.
by
rewrite
/
IntoVal
/
IntoDVal
=>
/
of_to_val
->.
Qed
.
theories/vcgen/vcgen.v
0 → 100644
View file @
0713b216
From
iris
.
heap_lang
Require
Export
proofmode
notation
.
From
iris
.
bi
Require
Import
big_op
.
From
iris_c
.
vcgen
Require
Import
dval
.
From
iris_c
.
c_translation
Require
Import
monad
translation
proofmode
.
From
iris_c
.
lib
Require
Import
locking_heap
U
.
Section
vcg
.
Context
`
{
amonadG
Σ
}.
Inductive
wp_expr
:
=
|
Base
:
iProp
Σ
→
wp_expr
|
Inhale
:
dloc
→
(
dval
→
wp_expr
)
→
wp_expr
|
Exhale
:
dloc
→
dval
→
level
→
wp_expr
→
wp_expr
|
IsSome
{
A
}
:
doption
A
→
(
A
→
wp_expr
)
→
wp_expr
|
IsLoc
:
dval
→
(
dloc
→
wp_expr
)
→
wp_expr
|
UMod
:
wp_expr
→
wp_expr
|
Par
:
((
dval
→
iProp
Σ
)
→
wp_expr
)
→
((
dval
→
iProp
Σ
)
→
wp_expr
)
→
(
dval
→
dval
→
wp_expr
)
→
wp_expr
.
Arguments
Base
_
%
I
.
Fixpoint
wp_interp
(
E
:
list
loc
)
(
a
:
wp_expr
)
:
iProp
Σ
:
=
match
a
with
|
Base
P
=>
P
|
Inhale
dl
Φ
=>
∃
dv
,
dloc_interp
E
dl
↦
U
dval_interp
E
dv
∗
wp_interp
E
(
Φ
dv
)
|
Exhale
dl
dv
x
Φ
=>
dloc_interp
E
dl
↦
[
x
]
dval_interp
E
dv
-
∗
wp_interp
E
Φ
|
IsSome
dmx
Φ
=>
∃
x
,
⌜
doption_interp
dmx
=
Some
x
⌝
∧
wp_interp
E
(
Φ
x
)
|
IsLoc
dv
Φ
=>
∃
dl
:
dloc
,
⌜
dval_interp
E
dv
=
#(
dloc_interp
E
dl
)
⌝
∧
wp_interp
E
(
Φ
dl
)
|
UMod
P
=>
U
(
wp_interp
E
P
)
|
Par
P1
P2
P3
=>
∃
(
Ψ
1
Ψ
2
:
dval
→
iProp
Σ
),
wp_interp
E
(
P1
Ψ
1
)
∗
wp_interp
E
(
P2
Ψ
2
)
∗
∀
(
dv1
dv2
:
dval
),
Ψ
1
dv1
-
∗
Ψ
2
dv2
-
∗
wp_interp
E
(
P3
dv1
dv2
)
end
%
I
.
Fixpoint
wp_interp_sane
(
E
:
list
loc
)
(
a
:
wp_expr
)
:
iProp
Σ
:
=
match
a
with
|
Base
Φ
=>
Φ
|
Inhale
dl
Φ
=>
∃
v
,
dloc_interp
E
dl
↦
U
v
∗
wp_interp_sane
E
(
Φ
(
dValUnknown
v
))
|
Exhale
dl
dv
x
Φ
=>
dloc_interp
E
dl
↦
[
x
]
dval_interp
E
dv
-
∗
wp_interp_sane
E
Φ
|
IsSome
dmx
Φ
=>
∃
x
,
⌜
doption_interp
dmx
=
Some
x
⌝
∧
wp_interp_sane
E
(
Φ
x
)
|
IsLoc
dv
Φ
=>
∃
l
:
loc
,
⌜
dval_interp
E
dv
=
#
l
⌝
∧
wp_interp_sane
E
(
Φ
(
dLocUnknown
l
))
|
UMod
P
=>
U
(
wp_interp_sane
E
P
)
|
Par
P1
P2
P3
=>
∃
Ψ
1
Ψ
2
:
val
→
iProp
Σ
,
wp_interp_sane
E
(
P1
(
λ
dv
,
Ψ
1
(
dval_interp
E
dv
)))
∗
wp_interp_sane
E
(
P2
(
λ
dv
,
Ψ
2
(
dval_interp
E
dv
)))
∗
∀
v1
v2
,
Ψ
1
v1
-
∗
Ψ
2
v2
-
∗
wp_interp_sane
E
(
P3
(
dValUnknown
v1
)
(
dValUnknown
v2
))
end
%
I
.
Lemma
wp_interp_sane_sound
E
a
:
wp_interp_sane
E
a
⊢
wp_interp
E
a
.
Proof
.
generalize
dependent
E
.
induction
a
.
-
done
.
-
simpl
.
iIntros
(
E
)
"He"
.
iDestruct
"He"
as
(
v
)
"[H1 H2]"
.
iExists
(
dValUnknown
v
).
simpl
.
iFrame
.
by
iApply
H0
.
-
simpl
.
iIntros
(
E
)
"He H"
.
iApply
IHa
.
by
iApply
"He"
.
-
simpl
.
iIntros
(
E
)
"He"
.
iDestruct
"He"
as
(
v
)
"[H1 H2]"
.
iExists
v
.
iFrame
.
by
iApply
H0
.
-
simpl
.
iIntros
(
E
)
"He"
.
iDestruct
"He"
as
(
l
)
"[H1 H2]"
.
iExists
(
dLocUnknown
l
).
simpl
.
iFrame
.
by
iApply
H0
.
-
simpl
.
intros
E
.
by
apply
U_mono
.
-
simpl
.
intros
E
.
iDestruct
1
as
(
Ψ
1
Ψ
2
)
"(HΨ1 & HΨ2 & HΦ)"
.
iExists
(
λ
dv
,
Ψ
1
(
dval_interp
E
dv
)),
(
λ
dv
,
Ψ
2
(
dval_interp
E
dv
)).
iSplitL
"HΨ1"
.
by
iApply
H0
.
iSplitL
"HΨ2"
.
by
iApply
H1
.
iIntros
(
dv1
dv2
)
"Hv1 Hv2"
.
iApply
H2
.
iApply
(
"HΦ"
with
"Hv1 Hv2"
).
Qed
.
Class
AWpQuote
(
E
:
list
loc
)
(
e
:
expr
)
(
R
:
iProp
Σ
)
(
Φ
:
dval
→
wp_expr
)
(
t
:
wp_expr
)
:
=
wp_quote
:
wp_interp
E
t
⊢
awp
e
R
(
λ
v
,
∃
dv
,
⌜
dval_interp
E
dv
=
v
⌝
∧
wp_interp
E
(
Φ
dv
)).
Global
Instance
awp_quote_default
E
e
R
Φ
:
AWpQuote
E
e
R
Φ
(
Base
(
awp
e
R
(
λ
v
,
wp_interp
E
(
Φ
(
dValUnknown
v
)))))
|
1000
.
Proof
.
rewrite
/
AWpQuote
/=.
iIntros
"H"
.
iApply
(
awp_wand
with
"H"
).
iIntros
(
v
)
"H"
.
iExists
(
dValUnknown
v
)
;
auto
.
Qed
.
(* TODO: awp ret for a general expression *)
Instance
awp_quote_ret
E
e
dv
R
Φ
:
IntoDVal
E
e
dv
→
AWpQuote
E
(
a_ret
e
)
R
Φ
(
Φ
dv
).
Proof
.
rewrite
/
AWpQuote
.
iIntros
(->)
"H"
.
iApply
awp_ret
.
iApply
wp_value
.
eauto
.
Qed
.
Global
Instance
awp_quote_load
E
e
R
Φ
t
:
AWpQuote
E
e
R
(
λ
dv
,
IsLoc
dv
(
λ
l
,
Inhale
l
(
λ
w
,
Exhale
l
w
ULvl
(
Φ
w
))))
t
→
AWpQuote
E
(
a_load
e
)
R
Φ
t
.
Proof
.
rewrite
/
AWpQuote
/=
=>
->.
iIntros
"H"
.
awp_apply
(
a_wp_awp
with
"H"
).
iIntros
(
a
)
"Ha"
.
iApply
a_load_spec
.
iApply
(
awp_wand
with
"Ha"
).
iIntros
(?).
iDestruct
1
as
(
dv
<-
l
->
w
)
"[Hl H]"
.
iExists
_
,
_;
iSplit
;
eauto
.
iFrame
"Hl"
.
iIntros
"Hl"
.
iExists
_;
iSplit
;
eauto
.
by
iApply
"H"
.
Qed
.
Global
Instance
wp_quote_store
E
e1
e2
R
Φ
(
t1
t2
:
((
dval
→
iProp
Σ
)
→
wp_expr
))
:
(
∀
Ψ
1
:
dval
→
iProp
Σ
,
AWpQuote
E
e1
R
(
λ
v1
,
IsLoc
v1
(
λ
l
,
Base
(
Ψ
1
(
dValUnknown
#(
dloc_interp
E
l
)))))
(
t1
Ψ
1
))
→
(
∀
Ψ
2
:
dval
→
iProp
Σ
,
AWpQuote
E
e2
R
(
λ
v
,
Base
(
Ψ
2
(
dValUnknown
(
dval_interp
E
v
))))
(
t2
Ψ
2
))
→
AWpQuote
E
(
a_store
e1
e2
)
R
Φ
(
Par
t1
t2
(
λ
v1
v2
,
IsLoc
v1
(
λ
l
,
Inhale
l
(
λ
_
,
Exhale
l
v2
LLvl
(
Φ
v2
))))).
Proof
.
rewrite
/
AWpQuote
/=
=>
He1
He2
.
iDestruct
1
as
(
Ψ
1
Ψ
2
)
"(HΨ1 & HΨ2 & HΦ)"
.
iApply
(
a_store_spec
_
_
(
λ
l
,
Ψ
1
(
dValUnknown
#
l
))
(
λ
v
,
Ψ
2
(
dValUnknown
v
))
with
"[HΨ1] [HΨ2]"
).
-
iPoseProof
(
He1
with
"HΨ1"
)
as
"H"
.
iApply
(
awp_wand
with
"H"
).
iIntros
(?).
iDestruct
1
as
(
dv
<-
dl
?)
"HΨ1"
.
iExists
_
.
iSplit
;
eauto
.
-
iPoseProof
(
He2
with
"HΨ2"
)
as
"H"
.
iApply
(
awp_wand
with
"H"
).
iIntros
(?).
iDestruct
1
as
(
dv
<-)
"$"
.
-
iNext
.
iIntros
(
l
w
)
"HΨ1 HΨ2"
.
iDestruct
(
"HΦ"
with
"HΨ1 HΨ2"
)
as
(
dl
?)
"H"
.
iDestruct
"H"
as
(
dv
)
"[Hl H]"
.
simplify_eq
/=.
iExists
_;
iFrame
.
iIntros
"Hl"
.
iExists
(
dValUnknown
w
)
;
iSplit
;
eauto
.
by
iApply
"H"
.
Qed
.
(*
Global Instance wp_quote_bin_op E op e1 e2 Φ Ψ t :
(∀ dv1, WpQuote E e2 (λ dv2, IsSome (dbin_op_eval E op dv1 dv2) Φ) (Ψ dv1)) →
WpQuote E e1 Ψ t → WpQuote E (BinOp op e1 e2) Φ t.
Proof.
rewrite /WpQuote /= => He2 ->. iIntros "H".
wp_apply (wp_wand with "H"); iIntros (v1).
iDestruct 1 as (dv <-) "H". rewrite He2.
wp_apply (wp_wand with "H"); iIntros (v2).
iDestruct 1 as (dv' <- w ?) "H".
wp_op.
- by apply dbin_op_eval_correct.
- iExists w. auto.
Qed.
Global Instance wp_quote_seq E e1 e2 Φ Ψ t `{Closed [] e2}:
WpQuote E e2 Φ Ψ →
WpQuote E e1 (λ _, Ψ) t →
WpQuote E (e1 ;; e2) Φ t.
Proof.
rewrite /WpQuote /= => He2 ->. iIntros "H".
wp_apply (wp_wand with "H"). iIntros (v1).
iDestruct 1 as (dv1 <-) "H". wp_seq.
by rewrite He2.
Qed.
*)
Fixpoint
exhale_list
(
s
:
list
(
nat
*
dval
))
(
Φ
:
wp_expr
)
:
wp_expr
:
=
match
s
with
|
(
i
,
v
)
::
s'
=>
Exhale
(
dLoc
i
)
v
ULvl
(
exhale_list
s'
Φ
)
|
[]
=>
Φ
end
.
Definition
exhale_list_interp
E
(
pl
:
list
(
nat
*
dval
))
:
iProp
Σ
:
=
([
∗
list
]
lw
∈
pl
,
dloc_interp
E
(
dLoc
lw
.
1
)
↦
U
dval_interp
E
lw
.
2
)%
I
.
Lemma
vcg_exhale_list_sound'
E
s
t
:
wp_interp
E
(
exhale_list
s
t
)
-
∗
exhale_list_interp
E
s
-
∗
wp_interp
E
t
.
Proof
.
unfold
exhale_list_interp
.
induction
s
as
[|
[
i
w
]
s'
]
;
simpl
.
-
by
iIntros
"$ _"
.
-
iIntros
"H [H1 H2]"
.
iSpecialize
(
"H"
with
"H1"
).
iApply
(
IHs'
with
"H H2"
).
Qed
.
Fixpoint
find_and_remove
(
pl
:
list
(
nat
*
dval
))
(
dl
:
dloc
)
:
option
(
list
(
nat
*
dval
)
*
dval
)
:
=
match
pl
with
|
[]
=>
None
|
(
i
,
v
)
::
pl'
=>
if
(
bool_decide
(
dl
=
dLoc
i
))
then
Some
(
pl'
,
v
)
else
match
find_and_remove
pl'
dl
with
|
None
=>
None
|
Some
(
rl
,
w
)
=>
Some
((
i
,
v
)
::
rl
,
w
)
end
end
.
Lemma
find_and_remove_dLocUnknown
pl
l
:
find_and_remove
pl
(
dLocUnknown
l
)
=
None
.
Proof
.
induction
pl
as
[|[?
?]
?]
;
eauto
;
simpl
;
by
rewrite
IHpl
.
Qed
.
Lemma
find_and_remove_dLocKnown
pl
pl'
d
w'
:
find_and_remove
pl
d
=
Some
(
pl'
,
w'
)
→
∃
i
,
d
=
dLoc
i
.
Proof
.
case
d
;
eauto
;
intros
?
;
rewrite
find_and_remove_dLocUnknown
;
inversion
1
.
Qed
.
Lemma
find_and_remove_big_sepL
pl
i
pl'
w'
(
Φ
:
nat
*
dval
→
iProp
Σ
)
:
find_and_remove
pl
(
dLoc
i
)
=
Some
(
pl'
,
w'
)
→
([
∗
list
]
lw
∈
pl
,
Φ
lw
)%
I
⊣
⊢
(([
∗
list
]
lw
∈
pl'
,
Φ
lw
)
∗
Φ
(
i
,
w'
))%
I
.
Proof
.
iIntros
(
Hfind
).
iInduction
pl
as
[|
hd
tl
]
"IH"
forall
(
pl'
Hfind
)
;
simpl
;
iSplit
;
try
(
done
||
simpl
in
H0
;
case_bool_decide
;
simplify_eq
/=
;
iIntros
"[H1 H2]"
;
iFrame
)
;
simpl
in
Hfind
;
destruct
hd
;
iIntros
"[HΦ Hlst]"
;
case_bool_decide
;
simplify_eq
/=
;
[
iFrame
|
|
iFrame
|].
-
destruct
(
find_and_remove
tl
(
dLoc
i
))
;
simplify_eq
/=.
destruct
p
;
simplify_eq
/=.
iFrame
.
by
iApply
"IH"
.
-
destruct
(
find_and_remove
tl
(
dLoc
i
))
;
simplify_eq
/=.
destruct
p
;
simplify_eq
/=.
iDestruct
"HΦ"
as
"[HΦ Hl]"
.
iFrame
.
iApply
(
"IH"
$!
l
)
;
first
done
.
iFrame
.
Qed
.
Fixpoint
mem
(
s
:
list
(
nat
*
dval
))
(
i
:
nat
)
:
bool
:
=
match
s
with
|
[]
=>
false
|
(
j
,
_
)
::
s'
=>
if
(
bool_decide
(
i
=
j
))
then
true
else
mem
s'
i
end
.
Lemma
mem_no_dup
s
i
:
false
=
mem
s
i
→
i
∉
s
.*
1
.
Proof
.
induction
s
;
intros
Hf
.
-
by
apply
not_elem_of_nil
.
-
apply
not_elem_of_cons
.
simpl
in
Hf
.
destruct
a
as
[
i'
?].
case_bool_decide
;
first
done
.
naive_solver
.
Qed
.
Fixpoint
optimize
(
s
:
list
(
nat
*
dval
))
(
Φ
:
wp_expr
)
:
wp_expr
:
=
match
Φ
with
|
Base
Φ
1
=>
exhale_list
s
Φ
|
Inhale
dl
Φ
1
=>
match
find_and_remove
s
dl
with
|
None
=>
Inhale
dl
(
λ
v
,
optimize
s
(
Φ
1
v
))
|
Some
(
s'
,
w
)
=>
optimize
s'
(
Φ
1
w
)
end
|
Exhale
(
dLoc
i
)
w
ULvl
Φ
=>
if
mem
s
i
then
Base
False
else
optimize
((
i
,
w
)
::
s
)
Φ
|
Exhale
(
dLoc
i
)
w
LLvl
Φ
=>
Exhale
(
dLoc
i
)
w
LLvl
(
optimize
s
Φ
)
|
Exhale
(
dLocUnknown
l
)
w
x
Φ
=>
Exhale
(
dLocUnknown
l
)
w
x
(
optimize
s
Φ
)
|
IsSome
dmx
Φ
1
=>
match
dmx
with
|
dNone
=>
Base
False
|
dSome
x
=>
optimize
s
(
Φ
1
x
)
|
_
=>
IsSome
dmx
(
λ
v
,
optimize
s
(
Φ
1
v
))
end
|
IsLoc
dv
Φ
1
=>
match
dv
with
|
dLitV
(
dLitLoc
l
)
=>
optimize
s
(
Φ
1
l
)
|
dLitV
(
dLitUnknown
_
)
|
dValUnknown
_
=>
IsLoc
dv
(
λ
v
,
optimize
s
(
Φ
1
v
))
|
_
=>
Base
False
end
|
UMod
P
=>
UMod
(
optimize
s
P
)
|
Par
P1
P2
P3
=>
Par
(
λ
Ψ
1
,
optimize
s
(
P1
Ψ
1
))
(
λ
Ψ
2
,
optimize
s
(
P2
Ψ
2
))
(
λ
v1
v2
,
optimize
s
(
P3
v1
v2
))
end
.
Lemma
vcg_opt_list_sound'
(
E
:
list
loc
)
(
pl
:
list
(
nat
*
dval
))
(
Φ
:
wp_expr
)
:
wp_interp
E
(
optimize
pl
Φ
)
-
∗
exhale_list_interp
E
pl
-
∗
(
wp_interp
E
Φ
).
Proof
.
(*
generalize dependent pl.
induction Φ; simpl.
- intros. eapply vcg_exhale_list_sound'.
- intros pl.
remember (find_and_remove pl d) as far. destruct far.
+ iIntros "Hw He".
destruct d; last by rewrite find_and_remove_dLocUnknown in Heqfar.
unfold exhale_list_interp. symmetry in Heqfar. destruct p.
apply find_and_remove_big_sepL
with (Φ := λ lw, (dloc_interp E (dLoc lw.1) ↦ dval_interp E lw.2)%I)
in Heqfar. rewrite Heqfar.
iDestruct "He" as "[Hlst Hp]".
iExists d. iFrame. rewrite H0. by iApply "Hw".
+ iIntros "Hwp Hexh". simplify_eq /=.
iDestruct "Hwp" as (d0) "[Hp Hwp]". rewrite H0.
iExists d0. iFrame. by iApply "Hwp".
- intros pl.
destruct d as [i|l].
+ remember (mem pl i) as msi. destruct msi.
{ iIntros "?"; done. }
iIntros "Hwp Hl Hi". rewrite IHΦ /exhale_list_interp.
iApply "Hwp". rewrite big_opL_cons. iFrame.
+ simpl. iIntros "Hwp Hexh Hl".