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
ca87e38f
Commit
ca87e38f
authored
Jul 01, 2018
by
Dan Frumin
Browse files
Finish the rest of the tests
parent
6f390922
Changes
10
Hide whitespace changes
Inline
Side-by-side
_CoqProject
View file @
ca87e38f
...
...
@@ -23,6 +23,5 @@ theories/vcgen/tests/swap.v
theories/vcgen/tests/fact.v
theories/tests/test1.v
theories/tests/test2.v
theories/tests/fact.v
theories/tests/gcd.v
theories/tests/lists.v
theories/c_translation/derived.v
View file @
ca87e38f
...
...
@@ -32,10 +32,10 @@ Section derived.
(
∀
l
:
loc
,
(
l
,
O
)
↦
C
∗
replicate
n
ev2
-
∗
Φ
(
cloc_to_val
(
l
,
O
)))
-
∗
awp
(
a_alloc
(
a_ret
e1
)
(
a_ret
e2
))
R
Φ
.
Proof
.
iIntros
(?
?
?)
"H"
.
iApply
(
a_alloc_spec
_
_
(
λ
v
,
⌜
v
=
#
n
⌝
)%
I
(
λ
v
,
⌜
v
=
ev2
⌝
)%
I
).
iIntros
(?
?
?)
"H"
.
iApply
(
a_alloc_spec
_
_
(
λ
v
,
⌜
v
=
#
n
⌝
)%
I
).
-
iApply
awp_ret
.
by
iApply
wp_value
.
-
iApply
awp_ret
.
by
iApply
wp_value
.
-
iNext
.
iIntros
(?
?
->
->).
iExists
n
;
iSplit
;
eauto
.
-
iApply
awp_ret
.
wp_value
_head
.
iNext
.
iIntros
(?
->).
iExists
n
;
iSplit
;
eauto
.
Qed
.
Lemma
a_store_ret
(
cl
:
cloc
)
(
e
:
expr
)
`
{
Closed
[]
e
}
R
Φ
:
...
...
@@ -56,10 +56,10 @@ Section derived.
Ltac
awp_ret_value
:
=
iApply
awp_ret
;
iApply
wp_value
;
eauto
.
Ltac
awp_alloc_ret
r
h
:
=
iApply
a_alloc_ret
;
iIntros
(
r
)
h
;
awp_lam
.
(*
Lemma awp_bin_op_load_load op (l r : loc) (v1 v2: val) R Φ :
Lemma
awp_bin_op_load_load
op
(
l
r
:
c
loc
)
(
v1
v2
:
val
)
R
Φ
:
l
↦
C
v1
-
∗
r
↦
C
v2
-
∗
(
l
↦
C
v1
-
∗
r
↦
C
v2
-
∗
∃
w
:
val
,
⌜
bin_op_eval
op
v1
v2
=
Some
w
⌝
∧
Φ
w
)
-
∗
awp (a_bin_op op (a_load (a_ret
#l
)) (a_load (a_ret
#r
))) R Φ.
awp
(
a_bin_op
op
(
a_load
(
a_ret
(
cloc_to_val
l
)
))
(
a_load
(
a_ret
(
cloc_to_val
r
)
)))
R
Φ
.
Proof
.
iIntros
"Hl Hr HΦ"
.
iApply
(
a_bin_op_spec
_
_
...
...
@@ -71,14 +71,14 @@ Section derived.
iApply
(
"HΦ"
with
"[$Hl] [$Hr]"
).
Qed
.
Lemma a_move_spec (s t :loc) (v w: val) R Φ :
Lemma
a_move_spec
(
s
t
:
c
loc
)
(
v
w
:
val
)
R
Φ
:
s
↦
C
v
∗
t
↦
C
w
∗
(
t
↦
C
w
-
∗
s
↦
C
[
LLvl
]
w
-
∗
Φ
w
)
-
∗
awp (a_store (a_ret
#s
) (a_load (a_ret
#t
))) R Φ.
awp
(
a_store
(
a_ret
(
cloc_to_val
s
)
)
(
a_load
(
a_ret
(
cloc_to_val
t
)
)))
R
Φ
.
Proof
.
iIntros
"(Hs & Ht & H)"
.
iApply
a_store_ret
.
awp_load_ret
t
.
iIntros
"Ht"
.
iExists
v
.
iFrame
.
iSpecialize
(
"H"
with
"Ht"
).
done
.
Qed.
*)
Qed
.
Lemma
a_invoke_simpl
(
ef
ea
:
expr
)
R
Φ
(
f
:
val
)
:
IntoVal
ef
f
→
...
...
theories/c_translation/translation.v
View file @
ca87e38f
...
...
@@ -105,20 +105,19 @@ Definition a_invoke: val := λ: "f" "arg",
Section
proofs
.
Context
`
{
amonadG
Σ
}.
Lemma
a_alloc_spec
R
Φ
Ψ
1
Ψ
2
e1
e2
:
Lemma
a_alloc_spec
R
Φ
Ψ
1 e1
e2
:
AWP
e1
@
R
{{
Ψ
1
}}
-
∗
AWP
e2
@
R
{{
Ψ
2
}}
-
∗
▷
(
∀
v1
v2
,
Ψ
1
v1
-
∗
Ψ
2
v2
-
∗
∃
n
:
nat
,
⌜
v1
=
#
n
⌝
∧
∀
l
,
(
l
,
O
)
↦
C
∗
replicate
n
v2
-
∗
Φ
(
cloc_to_val
(
l
,
O
)))
-
∗
AWP
e2
@
R
{{
v2
,
▷
(
∀
v1
,
Ψ
1
v1
-
∗
∃
n
:
nat
,
⌜
v1
=
#
n
⌝
∧
∀
l
,
(
l
,
O
)
↦
C
∗
replicate
n
v2
-
∗
Φ
(
cloc_to_val
(
l
,
O
)))
}}
-
∗
AWP
alloc
ᶜ
(
e1
,
e2
)
@
R
{{
Φ
}}.
Proof
.
iIntros
"H1
H2
HΦ"
.
iIntros
"H1 HΦ"
.
awp_apply
(
a_wp_awp
with
"H1"
)
;
iIntros
(
v1
)
"H1"
.
awp_lam
.
awp_apply
(
a_wp_awp
with
"H
2
"
)
;
iIntros
(
v2
)
"H2"
.
awp_lam
.
awp_apply
(
a_wp_awp
with
"H
Φ
"
)
;
iIntros
(
v2
)
"H2"
.
awp_lam
.
iApply
awp_bind
.
iApply
(
awp_par
with
"H1 H2"
).
iIntros
"!>"
(
w1
w2
)
"H1 H2 !>"
.
awp_let
.
do
2
(
awp_proj
;
awp_let
).
iDestruct
(
"H
Φ
"
with
"H1
H2
"
)
as
(
n
->)
"HΦ"
.
iDestruct
(
"H
2
"
with
"H1"
)
as
(
n
->)
"HΦ"
.
iApply
awp_atomic_env
.
iIntros
(
env
).
iDestruct
1
as
(
X
σ
HX
)
"[Hlocks Hσ]"
.
iIntros
"$"
.
wp_let
.
wp_apply
(
lreplicate_spec
with
"[//]"
)
;
iIntros
(
ll
Hll
).
...
...
theories/tests/fact.v
deleted
100644 → 0
View file @
6f390922
From
iris
.
heap_lang
Require
Export
proofmode
notation
.
From
iris
.
heap_lang
Require
Import
spin_lock
assert
par
.
From
iris
.
algebra
Require
Import
frac
auth
.
From
iris_c
.
lib
Require
Import
locking_heap
mset
flock
U
.
From
iris_c
.
c_translation
Require
Import
proofmode
translation
derived
.
Definition
incr
:
val
:
=
λ
:
"l"
,
a_store
(
a_ret
"l"
)
(
a_bin_op
PlusOp
(
a_load
(
a_ret
"l"
))
(
a_ret
#
1
)).
Definition
factorial_body
:
val
:
=
λ
:
"n"
"c"
"r"
,
a_while
(
λ
:
<>,
a_bin_op
LtOp
(
a_load
(
a_ret
"c"
))
(
a_ret
"n"
))
(
λ
:
<>,
incr
"c"
;
ᶜ
a_store
(
a_ret
"r"
)
(
a_bin_op
MultOp
(
a_load
(
a_ret
"r"
))
(
a_load
(
a_ret
"c"
)))).
Definition
factorial
:
val
:
=
λ
:
"n"
,
a_bind
(
λ
:
"r"
,
a_bind
(
λ
:
"k"
,
factorial_body
"n"
"k"
"r"
;
ᶜ
(
a_load
(
a_ret
"r"
)))
(
a_alloc
(
a_ret
#
0
%
V
)))
(
a_alloc
(
a_ret
#
1
%
V
)).
Section
factorial_spec
.
Context
`
{
amonadG
Σ
}.
Lemma
incr_spec
(
l
:
loc
)
(
n
:
Z
)
R
Φ
:
l
↦
C
#
n
-
∗
(
l
↦
C
[
LLvl
]
#(
n
+
1
)
-
∗
Φ
#(
n
+
1
))
-
∗
awp
(
incr
#
l
)
R
Φ
.
Proof
.
iIntros
"Hl HΦ"
.
awp_lam
.
iApply
(
a_store_ret
with
"[Hl HΦ]"
).
iApply
(
a_bin_op_spec
_
_
(
λ
v
,
⌜
v
=
#
n
⌝
∗
l
↦
C
#
n
)%
I
(
λ
v
,
⌜
v
=
#
1
⌝
)%
I
with
"[Hl] [] [HΦ]"
).
+
awp_load_ret
l
.
+
awp_ret_value
.
+
iNext
.
iIntros
(?
?)
"(% & Hc) %"
;
subst
.
iExists
#(
n
+
1
).
iSplit
;
eauto
with
iFrame
.
Qed
.
Lemma
factorial_body_spec
(
n
k
:
nat
)
(
c
r
:
loc
)
R
:
(
⌜
k
≤
n
⌝
∧
c
↦
C
[
ULvl
]
#
k
∗
r
↦
C
#(
fact
k
))
-
∗
awp
(
factorial_body
#
n
#
c
#
r
)
R
(
λ
_
,
c
↦
C
#
n
∗
r
↦
C
#(
fact
n
))%
I
.
Proof
.
iIntros
"(Hk & Hc & Hr)"
.
do
3
awp_lam
.
iL
ö
b
as
"IH"
forall
(
n
k
)
"Hk Hc Hr"
.
iApply
a_while_spec'
.
iNext
.
iApply
(
a_bin_op_spec
_
_
(
λ
v
,
⌜
v
=
#
k
⌝
∧
c
↦
C
#
k
)%
I
(
λ
v
,
⌜
v
=
#
n
⌝
)%
I
with
"[Hc]"
).
-
awp_load_ret
c
.
-
awp_ret_value
.
-
iNext
.
iIntros
(
v1
v2
)
"[% Hc] %"
;
subst
.
rewrite
/
bin_op_eval
/=.
iExists
_;
iSplit
;
eauto
.
case_bool_decide
.
+
iLeft
.
iSplit
;
eauto
.
iApply
a_sequence_spec'
.
iNext
.
iApply
(
incr_spec
with
"[$Hc]"
).
iIntros
"Hc"
.
iModIntro
.
iApply
(
a_store_ret
with
"[Hr Hc]"
).
iApply
(
a_bin_op_spec
_
_
(
λ
v
,
⌜
v
=
#(
fact
k
)
⌝
∗
r
↦
C
#(
fact
k
))%
I
(
λ
v
,
⌜
v
=
#(
k
+
1
)
⌝
∗
c
↦
C
#(
k
+
1
))%
I
with
"[Hr] [Hc]"
).
*
awp_load_ret
r
.
*
awp_load_ret
c
.
*
iNext
.
iIntros
(?
?)
"[% Hr] [% Hc]"
.
simplify_eq
.
rewrite
/
bin_op_eval
/=.
assert
((
fact
k
)
*
(
k
+
1
)
=
fact
(
k
+
1
))
as
->.
{
rewrite
Nat
.
add_1_r
/
fact
.
lia
.
}
iExists
#(
fact
(
k
+
1
))
;
repeat
(
iSplit
;
eauto
).
iExists
#(
fact
k
).
iFrame
.
iIntros
"Hr"
.
iModIntro
.
assert
(
Z_of_nat'
(
k
+
1
)%
nat
=
(
k
+
1
))
as
<-
by
lia
.
iApply
(
"IH"
$!
n
(
k
+
1
)%
nat
with
"[] Hc Hr"
).
iPureIntro
.
lia
.
+
iRight
.
iSplit
;
eauto
.
iApply
a_seq_spec
.
iModIntro
.
iDestruct
"Hk"
as
%
Hk
.
assert
(
k
=
n
)
as
->
by
lia
.
by
iFrame
.
Qed
.
Lemma
factorial_spec
(
n
:
nat
)
R
:
awp
(
factorial
#
n
)
R
(
λ
v
,
⌜
v
=
#(
fact
n
)
⌝
)%
I
.
Proof
.
awp_lam
.
iApply
awp_bind
.
awp_alloc_ret
r
"Hr"
.
iApply
awp_bind
.
awp_alloc_ret
c
"Hc"
.
iApply
a_sequence_spec
.
iNext
.
iApply
(
awp_wand
_
(
λ
_
,
c
↦
C
#
n
∗
r
↦
C
#(
fact
n
))%
I
with
"[Hr Hc]"
).
-
iApply
((
factorial_body_spec
n
0
c
r
)
with
"[$Hr $Hc]"
)
;
eauto
with
lia
.
-
iIntros
(?)
"[Hc Hr]"
.
iModIntro
.
awp_seq
.
awp_load_ret
r
.
Qed
.
Lemma
factorial_spec_with_inv
(
n
:
nat
)
R
:
awp
(
factorial
#
n
)
R
(
λ
v
,
⌜
v
=
#(
fact
n
)
⌝
)%
I
.
Proof
.
awp_lam
.
iApply
awp_bind
.
awp_alloc_ret
r
"Hr"
.
iApply
awp_bind
.
awp_alloc_ret
c
"Hc"
.
iApply
a_sequence_spec'
.
iNext
.
do
3
awp_lam
.
iApply
(
a_while_inv_spec
(
∃
k
:
nat
,
⌜
k
≤
n
⌝
∧
c
↦
C
#
k
∗
r
↦
C
#(
fact
k
))%
I
with
"[Hr Hc]"
).
-
iExists
O
.
eauto
with
iFrame
lia
.
-
iModIntro
.
iIntros
"H"
.
iDestruct
"H"
as
(
k
)
"(H & Hc & Hr)"
.
iApply
(
a_bin_op_spec
_
_
(
λ
v
,
⌜
v
=
#
k
⌝
∧
c
↦
C
#
k
)%
I
(
λ
v
,
⌜
v
=
#
n
⌝
)%
I
with
"[Hc]"
).
+
awp_load_ret
c
.
+
awp_ret_value
.
+
iNext
.
iIntros
(
v1
v2
)
"[% Hc] %"
;
subst
.
rewrite
/
bin_op_eval
/=.
iExists
_;
iSplit
;
eauto
.
case_bool_decide
.
*
iRight
.
iSplit
;
eauto
.
iNext
.
iApply
a_sequence_spec
.
iNext
.
iApply
(
incr_spec
with
"[$Hc]"
).
iIntros
"Hc"
.
iModIntro
.
awp_seq
.
iApply
(
a_store_ret
with
"[Hr Hc]"
).
iApply
(
a_bin_op_spec
_
_
(
λ
v
,
⌜
v
=
#(
fact
k
)
⌝
∗
r
↦
C
#(
fact
k
))%
I
(
λ
v
,
⌜
v
=
#(
k
+
1
)
⌝
∗
c
↦
C
#(
k
+
1
))%
I
with
"[Hr] [Hc]"
).
**
awp_load_ret
r
.
**
awp_load_ret
c
.
**
iNext
.
iIntros
(?
?)
"[% Hr] [% Hc]"
.
simplify_eq
.
rewrite
/
bin_op_eval
/=.
assert
((
fact
k
)
*
(
k
+
1
)
=
fact
(
k
+
1
))
as
->.
{
rewrite
Nat
.
add_1_r
/
fact
.
lia
.
}
iExists
#(
fact
(
k
+
1
))
;
repeat
(
iSplit
;
eauto
).
iExists
#(
fact
k
).
iFrame
.
iIntros
"Hr"
.
iModIntro
.
assert
(
Z_of_nat'
(
k
+
1
)%
nat
=
(
k
+
1
))
as
<-
by
lia
.
iExists
(
k
+
1
)%
nat
.
eauto
with
iFrame
lia
.
*
iLeft
.
iSplit
;
eauto
.
do
2
iModIntro
.
iRevert
"H"
.
iIntros
"%"
.
assert
(
k
=
n
)
as
->
by
lia
.
by
awp_load_ret
r
.
Qed
.
End
factorial_spec
.
theories/tests/gcd.v
View file @
ca87e38f
...
...
@@ -19,10 +19,10 @@ Definition gcd : val := λ: "a" "b",
Section
gcd_spec
.
Context
`
{
amonadG
Σ
}.
Lemma
gcd_spec
(
a
b
:
Z
)
(
l
r
:
loc
)
R
:
Lemma
gcd_spec
(
a
b
:
Z
)
(
l
r
:
c
loc
)
R
:
0
≤
a
→
0
≤
b
→
l
↦
C
#
a
-
∗
r
↦
C
#
b
-
∗
awp
(
gcd
#
l
#
r
)
R
(
λ
v
,
⌜
v
=
#(
Z
.
gcd
a
b
)
⌝
).
awp
(
gcd
(
cloc_to_val
l
)
(
cloc_to_val
r
)
)
R
(
λ
v
,
⌜
v
=
#(
Z
.
gcd
a
b
)
⌝
).
Proof
.
iIntros
(??)
"Hl Hr"
.
do
2
awp_lam
.
iApply
a_sequence_spec'
.
iNext
.
iApply
(
a_while_inv_spec
(
∃
x
y
:
Z
,
...
...
theories/tests/lists.v
View file @
ca87e38f
...
...
@@ -50,9 +50,9 @@ Definition in_place_reverse : val := λ: "hd",
a_list_store_next
(
a_load
(
a_ret
"i"
))
(
a_load
(
a_ret
"j"
))
;
ᶜ
a_store
(
a_ret
"j"
)
(
a_load
(
a_ret
"i"
))
;
ᶜ
a_store
(
a_ret
"i"
)
(
a_load
(
a_ret
"k"
)))
(
a_alloc
(
a_list_next
(
a_load
(
a_ret
"i"
)))))
;
ᶜ
(
a_alloc
♯
1
(
a_list_next
(
a_load
(
a_ret
"i"
)))))
;
ᶜ
(
a_load
(
a_ret
"j"
))
)
(
a_alloc
(
a_ret
NONEV
)))
(
a_alloc
(
a_ret
"hd"
)).
)
(
a_alloc
♯
1
(
a_ret
NONEV
)))
(
a_alloc
♯
1
(
a_ret
"hd"
)).
Section
list_spec
.
Context
`
{
amonadG
Σ
}.
...
...
@@ -60,7 +60,7 @@ Section list_spec.
Fixpoint
is_list
(
hd
:
val
)
(
xs
:
list
val
)
:
iProp
Σ
:
=
match
xs
with
|
[]
=>
⌜
hd
=
NONEV
⌝
|
x
::
xs
=>
∃
(
l
:
loc
)
hd'
,
⌜
hd
=
SOMEV
#
l
⌝
∗
l
↦
C
(
x
,
hd'
)
∗
is_list
hd'
xs
|
x
::
xs
=>
∃
(
l
:
c
loc
)
hd'
,
⌜
hd
=
SOMEV
(
cloc_to_val
l
)
⌝
∗
l
↦
C
(
x
,
hd'
)
∗
is_list
hd'
xs
end
%
I
.
Lemma
a_list_nil_spec
R
Φ
:
...
...
@@ -69,7 +69,7 @@ Section list_spec.
Lemma
a_list_next_spec
(
e
:
expr
)
R
Φ
:
awp
e
R
(
λ
v
,
∃
(
l
:
loc
)
hd
x
xs
,
⌜
v
=
SOMEV
#
l
⌝
∧
l
↦
C
(
x
,
hd
)
∗
is_list
hd
xs
∗
∃
(
l
:
c
loc
)
hd
x
xs
,
⌜
v
=
SOMEV
(
cloc_to_val
l
)
⌝
∧
l
↦
C
(
x
,
hd
)
∗
is_list
hd
xs
∗
(
l
↦
C
(
x
,
hd
)
-
∗
is_list
hd
xs
-
∗
Φ
hd
))
-
∗
awp
(
a_list_next
e
)
R
Φ
.
Proof
.
...
...
@@ -87,10 +87,10 @@ Section in_place_reversal.
Context
`
{
amonadG
Σ
}.
Lemma
a_list_store_next_spec
e1
e2
Ψ
1
Ψ
2
R
Φ
:
awp
e1
R
(
λ
v
,
∃
(
hd
:
loc
)
x
old
,
⌜
v
=
SOMEV
#
hd
⌝
∧
hd
↦
C
(
x
,
old
)
∗
Ψ
1
(
x
,
SOMEV
#
hd
))
-
∗
awp
e1
R
(
λ
v
,
∃
(
hd
:
c
loc
)
x
old
,
⌜
v
=
SOMEV
(
cloc_to_val
hd
)
⌝
∧
hd
↦
C
(
x
,
old
)
∗
Ψ
1
(
x
,
SOMEV
(
cloc_to_val
hd
))
)
-
∗
awp
e2
R
Ψ
2
-
∗
(
∀
(
hd
:
loc
)
x
new
,
Ψ
1
(
x
,
SOMEV
#
hd
)
-
∗
Ψ
2
new
-
∗
(
∀
(
hd
:
c
loc
)
x
new
,
Ψ
1
(
x
,
SOMEV
(
cloc_to_val
hd
)
)
-
∗
Ψ
2
new
-
∗
(
hd
↦
C
[
LLvl
]
(
x
,
new
)
-
∗
Φ
(
x
,
new
)%
V
))
-
∗
awp
(
a_list_store_next
e1
e2
)
R
Φ
.
Proof
.
...
...
@@ -111,42 +111,48 @@ Section in_place_reversal.
awp
(
in_place_reverse
hd
)
R
(
λ
v
,
is_list
v
(
reverse
xs
)).
Proof
.
iIntros
"Hlst"
.
awp_lam
.
iApply
awp_bind
;
awp_alloc_ret
i
"Hi"
.
iApply
awp_bind
;
awp_alloc_ret
j
"Hj"
.
iApply
awp_bind
;
awp_alloc_ret
i
"
[
Hi
_]
"
.
iApply
awp_bind
;
awp_alloc_ret
j
"
[
Hj
_]
"
.
iApply
a_sequence_spec'
.
iNext
.
iApply
(
a_while_inv_spec
(
∃
ls
rs
rhd
hd
,
i
↦
C
hd
∗
is_list
hd
ls
∗
j
↦
C
rhd
∗
is_list
rhd
rs
∧
⌜
(
reverse
rs
)++
ls
=
xs
⌝
)%
I
with
"[Hlst Hj Hi]"
).
iApply
(
a_while_inv_spec
(
∃
ls
rs
rhd
hd
,
(
i
,
O
)
↦
C
hd
∗
is_list
hd
ls
∗
(
j
,
O
)
↦
C
rhd
∗
is_list
rhd
rs
∧
⌜
(
reverse
rs
)++
ls
=
xs
⌝
)%
I
with
"[Hlst Hj Hi]"
).
-
iExists
xs
,
[],
(
InjLV
#()),
hd
;
eauto
with
iFrame
.
-
iModIntro
;
iIntros
"H"
.
clear
hd
.
iDestruct
"H"
as
(
ls
rs
rhd
hd
)
"(Hi & Hls & Hj & Hrs & %)"
.
iApply
a_un_op_spec
.
iApply
(
a_bin_op_spec
_
_
(
λ
x
,
⌜
x
=
hd
⌝
∧
i
↦
C
hd
)%
I
(
λ
x
,
⌜
x
=
NONEV
⌝
)%
I
with
"[Hi] [] [-]"
).
{
awp_load_ret
i
.
}
{
awp_ret_value
.
}
(
λ
x
,
⌜
x
=
hd
⌝
∧
(
i
,
O
)
↦
C
hd
)%
I
(
λ
x
,
⌜
x
=
NONEV
⌝
)%
I
with
"[Hi] [] [-]"
).
{
awp_load_ret
(
i
,
O
)
.
}
{
awp_ret_value
.
}
iNext
.
iIntros
(?
?)
"[-> Hi ] ->"
.
destruct
ls
.
+
rewrite
{
1
}/
is_list
.
iDestruct
"Hls"
as
"->"
.
iExists
#
true
;
iSplit
;
first
done
.
iExists
#
false
;
iSplit
;
first
done
.
iLeft
;
iSplit
;
first
done
.
do
2
iModIntro
.
awp_load_ret
j
.
iLeft
;
iSplit
;
first
done
.
do
2
iModIntro
.
awp_load_ret
(
j
,
O
)
.
iIntros
"_"
.
simplify_eq
/=.
by
rewrite
app_nil_r
reverse_involutive
.
+
iDestruct
"Hls"
as
(
l
lnxt
)
"(-> & Hl & Hls)"
.
fold
is_list
.
iExists
#
false
;
iSplit
;
first
done
;
iExists
#
true
;
iSplit
;
first
done
.
iRight
.
iSplit
;
first
done
.
iApply
awp_bind
.
iNext
.
iApply
a_alloc_spec
.
iApply
a_list_next_spec
.
awp_load_ret
i
.
iIntros
"Hi"
.
iExists
l
,
lnxt
,
v
,
ls
.
iNext
.
iApply
(
a_alloc_spec
_
_
(
λ
v
,
⌜
v
=
#
1
⌝
)
with
"[] [-]"
)%
I
.
{
iApply
awp_ret
.
by
wp_value_head
.
}
iApply
a_list_next_spec
.
awp_load_ret
(
i
,
O
).
iIntros
"Hi"
.
iExists
l
,
lnxt
,
v
,
ls
.
iSplit
;
first
done
.
iFrame
.
iIntros
"Hl Hls"
.
iIntros
(
k
)
"Hk"
.
awp_let
.
iApply
a_sequence_spec'
;
iNext
.
iNext
.
iIntros
(?
->).
iExists
1
%
nat
;
iSplit
;
eauto
.
iIntros
(
k
)
"[Hk _]"
.
awp_let
.
iApply
a_sequence_spec'
;
iNext
.
iApply
(
a_list_store_next_spec
_
_
(
λ
z
,
⌜
z
=
(
v
,
SOMEV
#
l
)
⌝
∧
i
↦
C
(
SOMEV
#
l
)
)%
I
(
λ
v
,
⌜
v
=
rhd
⌝
∧
j
↦
C
rhd
)%
I
with
"[Hi Hl] [Hj]"
).
{
awp_load_ret
i
.
eauto
42
with
iFrame
.
}
{
awp_load_ret
j
.
}
iIntros
(?
?
?)
"(% & Hi) (% & Hj)"
.
simplify_eq
.
(
λ
z
,
⌜
z
=
(
v
,
SOMEV
(
cloc_to_val
l
))
⌝
∧
(
i
,
O
)
↦
C
(
SOMEV
(
cloc_to_val
l
))
)%
I
(
λ
v
,
⌜
v
=
rhd
⌝
∧
(
j
,
O
)
↦
C
rhd
)%
I
with
"[Hi Hl] [Hj]"
).
{
awp_load_ret
(
i
,
O
).
eauto
42
with
iFrame
.
}
{
awp_load_ret
(
j
,
O
).
}
iIntros
(
a0
?
?)
"(% & Hi) (% & Hj)"
.
simplify_eq
/=.
(* TODO: this is annoying *)
assert
(
a0
=
l
)
as
->.
{
by
destruct
l
,
a0
;
simplify_eq
/=.
}
iIntros
"Hl"
.
iModIntro
.
iApply
a_sequence_spec'
;
iNext
.
iApply
(
a_move_spec
with
"[$Hj $Hi Hls Hrs Hk Hl]"
).
iIntros
"Hi Hj"
.
iModIntro
.
iApply
(
a_move_spec
with
"[$Hi $Hk Hls Hrs Hj Hl]"
).
iIntros
"Hk Hi"
.
iModIntro
.
iExists
ls
,
(
v
::
rs
),
(
InjRV
#
l
),
lnxt
.
iIntros
"Hk Hi"
.
iModIntro
.
iExists
ls
,
(
v
::
rs
),
(
InjRV
(
cloc_to_val
l
)
),
lnxt
.
iFrame
.
iSplit
.
*
iExists
l
,
rhd
;
iSplit
;
first
done
;
iFrame
.
*
iPureIntro
.
simplify_eq
.
by
rewrite
cons_middle
assoc
-
reverse_cons
.
Qed
.
End
in_place_reversal
.
theories/tests/test1.v
View file @
ca87e38f
...
...
@@ -47,8 +47,7 @@ Section test.
awp
(
swap
(
cloc_to_val
l1
)
(
cloc_to_val
l2
))
R
(
λ
_
,
l1
↦
C
v2
∗
l2
↦
C
v1
).
Proof
.
iIntros
"Hl1 Hl2"
.
do
2
awp_lam
.
iApply
awp_bind
.
iApply
(
a_alloc_ret
1
#
0
).
iIntros
(
r
)
"Hr"
.
awp_lam
.
do
2
awp_lam
.
iApply
awp_bind
.
awp_alloc_ret
r
"Hr"
.
iApply
a_sequence_spec'
.
iNext
.
...
...
theories/tests/test2.v
View file @
ca87e38f
...
...
@@ -8,12 +8,12 @@ From iris_c.c_translation Require Import proofmode translation derived.
Section
test
.
Context
`
{
amonadG
Σ
}.
Lemma
test_fractional
(
x
:
loc
)
:
Lemma
test_fractional
(
x
:
c
loc
)
:
x
↦
C
#
1
-
∗
awp
(
a_store
(
a_ret
#
x
)
(
a_bin_op
PlusOp
(
a_load
(
a_ret
#
x
))
(
a_load
(
a_ret
#
x
))))
True
(
λ
_
,
x
↦
C
[
LLvl
]
#
2
).
awp
(
a_store
(
a_ret
(
cloc_to_val
x
)
)
(
a_bin_op
PlusOp
(
a_load
(
a_ret
(
cloc_to_val
x
)
))
(
a_load
(
a_ret
(
cloc_to_val
x
)
))))
True
(
λ
_
,
x
↦
C
[
LLvl
]
#
2
).
Proof
.
iIntros
"[Hx Hx']"
.
iApply
(
a_store_spec
_
_
(
λ
v
,
⌜
v
=
#
x
⌝
)
(
λ
v
,
⌜
v
=
#
2
⌝
∗
x
↦
C
#
1
)
with
"[] [Hx Hx']"
)%
I
.
iApply
(
a_store_spec
_
_
(
λ
v
,
⌜
v
=
(
cloc_to_val
x
)
⌝
)
(
λ
v
,
⌜
v
=
#
2
⌝
∗
x
↦
C
#
1
)
with
"[] [Hx Hx']"
)%
I
.
{
iApply
awp_ret
.
wp_value_head
.
eauto
.
}
-
iApply
(
a_bin_op_spec
_
_
(
λ
v
,
⌜
v
=
#
1
⌝
∗
x
↦
C
{
1
/
2
}
#
1
)
(
λ
v
,
⌜
v
=
#
1
⌝
∗
x
↦
C
{
1
/
2
}
#
1
)
...
...
theories/vcgen/tests/swap.v
View file @
ca87e38f
...
...
@@ -14,47 +14,38 @@ Section tests_vcg.
(
a_store
(
a_ret
"l2"
)
(
a_load
(
a_ret
"r"
)))
;
ᶜ
(
a_ret
#
0
).
Lemma
swap_spec_by_vcg_opt
(
l1
l2
r
:
loc
)
(
v1
v2
:
val
)
R
:
Lemma
swap_spec_by_vcg_opt
(
l1
l2
r
:
c
loc
)
(
v1
v2
:
val
)
R
:
r
↦
C
#
0
-
∗
l1
↦
C
v1
∗
l2
↦
C
v2
-
∗
awp
(
swap
#
l1
#
l2
#
r
)
R
(
λ
_
,
l2
↦
C
v1
∗
l1
↦
C
v2
).
awp
(
swap
(
cloc_to_val
l1
)
(
cloc_to_val
l2
)
(
cloc_to_val
r
)
)
R
(
λ
_
,
l2
↦
C
v1
∗
l1
↦
C
v2
).
Proof
.
iIntros
"Hr [Hl1 Hl2]"
.
do
3
awp_lam
.
vcg_solver
.
iIntros
"!> !> !>"
.
eauto
with
iFrame
.
Qed
.
Definition
swap_with_alloc
:
val
:
=
λ
:
"l1"
"l2"
,
Definition
swap_with_alloc
:
val
:
=
λ
:
"l1"
"l2"
,
a_bind
(
λ
:
"r"
,
(
a_store
(
a_ret
"r"
)
(
a_load
(
a_ret
"l1"
)))
;
ᶜ
(
a_store
(
a_ret
"l1"
)
(
a_load
(
a_ret
"l2"
)))
;
ᶜ
((
a_store
(
a_ret
"l2"
)
(
a_load
(
a_ret
"r"
))))
;
ᶜ
a_ret
#())
(
a_alloc
(
a_ret
#
0
)
).
(
a_alloc
♯
1
♯
0
).
Lemma
swap_spec
(
l1
l2
:
loc
)
(
v1
v2
:
val
)
R
:
Lemma
load_spec
(
l
:
loc
)
(
v1
v2
:
val
)
R
:
(
l
,
1
%
nat
)
↦
C
v1
-
∗
AWP
∗ᶜ
(
a_ret
(#
l
,
#
1
))
@
R
{{
_
,
(
l
,
1
%
nat
)
↦
C
v1
}}.
Proof
.
iIntros
"Hl"
.
vcg_solver
.
eauto
.
Qed
.
Lemma
swap_spec
(
l1
l2
:
cloc
)
(
v1
v2
:
val
)
R
:
l1
↦
C
v1
-
∗
l2
↦
C
v2
-
∗
awp
(
swap_with_alloc
#
l1
#
l2
)
R
(
λ
_
,
l1
↦
C
v2
∗
l2
↦
C
v1
).
awp
(
swap_with_alloc
(
cloc_to_val
l1
)
(
cloc_to_val
l2
)
)
R
(
λ
_
,
l1
↦
C
v2
∗
l2
↦
C
v1
).
Proof
.
iIntros
"Hl1 Hl2"
.
do
2
awp_lam
.
iApply
awp_bind
.
awp_alloc_ret
r
"Hr"
.
do
2
awp_lam
.
iApply
awp_bind
.
awp_alloc_ret
r
"[Hr _]"
.
progress
compute
[
cloc_add
].
simpl
.
vcg_solver
.
iIntros
"!> !> !>"
.
eauto
with
iFrame
.
(* Compared with step-by-step proof *)
(*
do 2 awp_lam. iApply awp_bind. awp_alloc_ret r "Hr".
iApply a_sequence_spec'. iNext.
iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret l1. iIntros "Hl1". iExists #0. iFrame.
iIntros "Hr". iModIntro. iApply a_sequence_spec'. iNext.
iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret l2. iIntros "Hl2". iExists v1. iFrame.
iIntros "Hl1". iModIntro. iApply a_sequence_spec'. iNext.
iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret r. iIntros "Hr". iExists v2. iFrame.
iIntros "Hl2". iModIntro. awp_ret_value. by iFrame. *)
Qed
.
End
tests_vcg
.
theories/vcgen/tests/unknowns.v
View file @
ca87e38f
...
...
@@ -8,13 +8,13 @@ From iris_c.lib Require Import locking_heap U.
Section
tests_vcg
.
Context
`
{
amonadG
Σ
}.
Lemma
test1
(
l
k
:
loc
)
(
e
:
expr
)
`
{
Closed
[]
e
}
:
Lemma
test1
(
l
k
:
c
loc
)
(
e
:
expr
)
`
{
Closed
[]
e
}
:
□
(
∀
Φ
v
,
k
↦
C
v
-
∗
(
k
↦
C
#
12
-
∗
Φ
v
)
-
∗
awp
e
True
Φ
)
-
∗
l
↦
C
#
1
-
∗
k
↦
C
#
10
-
∗
awp
(
♯
l
=
ᶜ
♯
2
+
ᶜ
e
;
ᶜ
♯
l
=
ᶜ
e
)
(
♯
ₗ
l
=
ᶜ
♯
2
+
ᶜ
e
;
ᶜ
♯
ₗ
l
=
ᶜ
e
)
True
(
λ
v
,
True
).
Proof
.
iIntros
"#He Hl Hk"
.
vcg_solver
.
...
...
@@ -24,21 +24,22 @@ Section tests_vcg.
vcg_continue
.
eauto
.
Qed
.
Lemma
test2
(
k
:
loc
)
:
k
↦
C
#
10
-
∗
awp
(
alloc
ᶜ
♯
11
=
ᶜ
∗ᶜ♯
k
+
ᶜ
♯
2
)
True
(
λ
v
,
⌜
v
=
#
12
⌝
).
Lemma
test2
(
k
:
c
loc
)
:
k
↦
C
#
10
-
∗
awp
(
alloc
ᶜ
(
♯
2
,
♯
11
)
=
ᶜ
∗ᶜ♯
ₗ
k
+
ᶜ
♯
2
)
True
(
λ
v
,
⌜
v
=
#
12
⌝
).
Proof
.
iIntros
"Hk"
.
vcg_solver
.
iIntros
"Hk"
.
iApply
a_alloc_spec
.
vcg_solver
.
iIntros
"Hk"
(
l
)
"Hl"
.
iIntros
"Hk"
.
iApply
(
a_alloc_ret
2
).
iIntros
(
l
)
"[Hl1 [Hl2 _]]"
.
compute
[
cloc_add
].
simpl
.
vcg_continue
.
eauto
42
with
iFrame
.
Qed
.
Lemma
test6
(
l
k
:
loc
)
(
e1
e2
:
expr
)
`
{
Closed
[]
e1
,
Closed
[]
e2
}
:
Lemma
test6
(
l
k
:
c
loc
)
(
e1
e2
:
expr
)
`
{
Closed
[]
e1
,
Closed
[]
e2
}
:
(
∀
Φ
,
Φ
#
11
-
∗
awp
e1
True
Φ
)
-
∗
(
∀
Φ
,
Φ
#
12
-
∗
awp
e2
True
Φ
)
-
∗
l
↦
C
#
1
-
∗
k
↦
C
#
1
-
∗
AWP
(
♯
l
=
ᶜ
♯
2
)
+
ᶜ
(
♯
k
=
ᶜ
e1
;
ᶜ
e2
)
AWP
(
♯
ₗ
l
=
ᶜ
♯
2
)
+
ᶜ
(
♯
ₗ
k
=
ᶜ
e1
;
ᶜ
e2
)
{{
v
,
l
↦
C
[
LLvl
]
#
2
∗
k
↦
C
#
11
∧
⌜
v
=
#
14
⌝
}}.
Proof
.
iIntros
"He1 He2 Hl Hk"
.
vcg_solver
.
...
...
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