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
Actris
Commits
f5e2db76
Commit
f5e2db76
authored
Jul 04, 2019
by
Robbert Krebbers
Browse files
Make the `list` stuff simpler since we don't really use `val_encode` anymore.
parent
763ab7f7
Changes
9
Hide whitespace changes
Inline
Side-by-side
_CoqProject
View file @
f5e2db76
-Q theories osiris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/utils/auth_excl.v
theories/utils/encodable.v
theories/utils/list.v
theories/utils/compare.v
theories/utils/spin_lock.v
...
...
theories/utils
/encodable.v
→
experimental
/encodable.v
View file @
f5e2db76
File moved
theories/examples
/producer_consumer.v
→
experimental
/producer_consumer.v
View file @
f5e2db76
...
...
@@ -4,10 +4,8 @@ From iris.heap_lang Require Import proofmode notation.
From
iris
.
heap_lang
Require
Import
assert
.
From
osiris
.
utils
Require
Import
list
compare
spin_lock
.
Definition
qnew
:
val
:
=
λ
:
<>,
#().
Definition
qenqueue
:
val
:
=
λ
:
"q"
"v"
,
#().
Definition
qdequeue
:
val
:
=
λ
:
"q"
,
#().
Definition
qis_empty
:
val
:
=
λ
:
"q"
,
#().
Definition
enq
:
=
true
.
Definition
deq
:
=
false
.
...
...
@@ -23,10 +21,11 @@ Definition pd_loop : val :=
if
:
"cc"
≤
#
0
then
#()
else
if
:
recv
"c"
then
(* enq/deq *)
if
:
recv
"c"
then
(* cont/stop *)
"go"
(
qenqueue
"q"
(
recv
"c"
))
"pc"
"cc"
"c"
let
:
"x"
:
=
recv
"x"
in
"go"
(
qenqueue
"q"
"x"
)
"pc"
"cc"
"c"
else
"go"
"q"
(
"pc"
-#
1
)
"cc"
"c"
else
if
:
(
qis_empty
"q"
)
then
if
:
lisnil
"q"
then
if
:
"pc"
≤
#
0
then
send
"c"
#
stop
;;
"go"
"q"
"pc"
(
"cc"
-#
1
)
"c"
...
...
@@ -40,7 +39,7 @@ Definition pd_loop : val :=
"go"
(
Fst
"qv"
)
"pc"
"cc"
"c"
.
Definition
new_pd
:
val
:
=
λ
:
"pc"
"cc"
,
let
:
"q"
:
=
qnew
#()
in
let
:
"q"
:
=
lnil
#()
in
let
:
"c"
:
=
start_chan
(
λ
:
"c"
,
pd_loop
"q"
"pc"
"cc"
"c"
)
in
let
:
"l"
:
=
new_lock
#()
in
(
"c"
,
"l"
).
...
...
theories/channel/channel.v
View file @
f5e2db76
...
...
@@ -56,7 +56,7 @@ Section channel.
Context
`
{!
heapG
Σ
,
!
chanG
Σ
}
(
N
:
namespace
).
Definition
is_list_ref
(
l
:
val
)
(
xs
:
list
val
)
:
iProp
Σ
:
=
(
∃
l'
:
loc
,
⌜
l
=
#
l'
⌝
∧
l'
↦
val_encode
xs
)%
I
.
(
∃
l'
:
loc
,
⌜
l
=
#
l'
⌝
∧
l'
↦
llist
xs
)%
I
.
Record
chan_name
:
=
Chan_name
{
chan_lock_name
:
gname
;
...
...
@@ -139,7 +139,7 @@ Section channel.
(
vs
ws
)
"(Href & Hvs & Href' & Hws)"
.
iDestruct
"Href"
as
(
ll
Hslr
)
"Hll"
.
rewrite
Hslr
.
wp_load
.
wp_apply
(
lsnoc_spec
(
A
:
=
val
))=>
//
;
iIntros
(
_
).
wp_apply
(
lsnoc_spec
with
"[//]"
)
;
iIntros
(
_
).
wp_bind
(
_
<-
_
)%
E
.
iMod
"HΦ"
as
(
vs'
)
"[Hchan HΦ]"
.
iDestruct
(
excl_eq
with
"Hvs Hchan"
)
as
%<-%
leibniz_equiv
.
...
...
theories/examples/mapper.v
View file @
f5e2db76
...
...
@@ -140,8 +140,8 @@ Section mapper.
c
↣
mapper_protocol
n
(
X_send
:
gmultiset
A
)
@
N
∗
([
∗
list
]
x
;
v
∈
xs
;
vs
,
IA
x
v
)
∗
([
∗
list
]
x
;
w
∈
xs_recv
;
ws
,
IB
(
f
x
)
w
)
}}}
mapper_service_loop
#
n
c
(
val_encode
vs
)
(
val_encode
ws
)
{{{
ys
ws
,
RET
(
val_encode
ws
)
;
mapper_service_loop
#
n
c
(
llist
vs
)
(
llist
ws
)
{{{
ys
ws
,
RET
(
llist
ws
)
;
⌜
ys
≡
ₚ
f
<$>
elements
X_send
++
xs
⌝
∗
[
∗
list
]
y
;
w
∈
ys
++
(
f
<$>
xs_recv
)
;
ws
,
IB
y
w
}}}.
...
...
@@ -152,20 +152,20 @@ Section mapper.
{
destruct
Hn
as
[->
->]
;
first
lia
.
iApply
(
"HΦ"
$!
[])
;
simpl
.
rewrite
big_sepL2_fmap_l
.
auto
.
}
destruct
n
as
[|
n
]=>
//=.
wp_branch
as
%?|%
_;
wp_pures
.
-
wp_apply
(
lisnil_spec
(
A
:
=
val
)
with
"[//]"
)
;
iIntros
(
_
).
-
wp_apply
(
lisnil_spec
with
"[//]"
)
;
iIntros
(
_
).
destruct
vs
as
[|
v
vs
],
xs
as
[|
x
xs
]
;
csimpl
;
try
done
;
wp_pures
.
+
wp_select
.
wp_pures
.
rewrite
Nat2Z
.
inj_succ
Z
.
sub_1_r
Z
.
pred_succ
.
iApply
(
"IH"
with
"[] Hc [//] [$] HΦ"
).
iPureIntro
;
naive_solver
.
+
iDestruct
"HIA"
as
"[HIAx HIA]"
.
wp_select
.
wp_apply
(
lhead_spec
(
A
:
=
val
)
with
"[//]"
)
;
iIntros
(
_
).
wp_apply
(
lhead_spec
with
"[//]"
)
;
iIntros
(
_
).
wp_send
with
"[$HIAx]"
.
wp_apply
(
ltail_spec
(
A
:
=
val
)
with
"[//]"
)
;
iIntros
(
_
).
wp_apply
(
ltail_spec
with
"[//]"
)
;
iIntros
(
_
).
wp_apply
(
"IH"
with
"[] Hc HIA HIB"
)
;
first
done
.
iIntros
(
ys
ws'
).
rewrite
gmultiset_elements_disj_union
gmultiset_elements_singleton
-!
assoc_L
.
iApply
"HΦ"
.
-
wp_recv
(
x
w
)
as
(
HH
)
"HIBfx"
.
wp_apply
(
lcons_spec
(
A
:
=
val
)
with
"[//]"
)
;
iIntros
(
_
).
wp_apply
(
lcons_spec
with
"[//]"
)
;
iIntros
(
_
).
wp_apply
(
"IH"
$!
_
_
_
_
_
(
_
::
_
)
with
"[] Hc HIA [HIBfx HIB]"
)
;
first
done
.
{
simpl
;
iFrame
.
}
iIntros
(
ys
ws'
)
;
iDestruct
1
as
(
Hys
)
"HIB"
;
simplify_eq
/=.
...
...
@@ -182,9 +182,8 @@ Section mapper.
0
<
n
→
(
∀
x
v
,
{{{
IA
x
v
}}}
ff
v
{{{
w
,
RET
w
;
IB
(
f
x
)
w
}}})
-
∗
{{{
[
∗
list
]
x
;
v
∈
xs
;
vs
,
IA
x
v
}}}
mapper_service
#
n
ff
(
val_encode
vs
)
{{{
ys
ws
,
RET
(
val_encode
ws
)
;
⌜
ys
≡
ₚ
f
<$>
xs
⌝
∗
[
∗
list
]
y
;
w
∈
ys
;
ws
,
IB
y
w
}}}.
mapper_service
#
n
ff
(
llist
vs
)
{{{
ys
ws
,
RET
(
llist
ws
)
;
⌜
ys
≡
ₚ
f
<$>
xs
⌝
∗
[
∗
list
]
y
;
w
∈
ys
;
ws
,
IB
y
w
}}}.
Proof
.
iIntros
(?)
"#Hf !>"
;
iIntros
(
Φ
)
"HI HΦ"
.
wp_lam
;
wp_pures
.
wp_apply
(
new_lock_spec
N
with
"[//]"
)
;
iIntros
(
lk
)
"[Hu Hlk]"
.
...
...
theories/examples/sort.v
View file @
f5e2db76
...
...
@@ -43,42 +43,42 @@ Section sort.
`
{!
RelDecision
R
,
!
Total
R
}
(
cmp
:
val
),
MSG
cmp
{{
cmp_spec
I
R
cmp
}}
;
<!>
(
xs
:
list
A
)
(
l
:
loc
)
(
vs
:
list
val
),
MSG
#
l
{{
l
↦
val_encode
vs
∗
[
∗
list
]
x
;
v
∈
xs
;
vs
,
I
x
v
}}
;
MSG
#
l
{{
l
↦
llist
vs
∗
[
∗
list
]
x
;
v
∈
xs
;
vs
,
I
x
v
}}
;
<?>
(
xs'
:
list
A
)
(
vs'
:
list
val
),
MSG
#()
{{
⌜
Sorted
R
xs'
⌝
∗
⌜
xs'
≡
ₚ
xs
⌝
∗
l
↦
val_encode
vs'
∗
[
∗
list
]
x
;
v
∈
xs'
;
vs'
,
I
x
v
}}
;
l
↦
llist
vs'
∗
[
∗
list
]
x
;
v
∈
xs'
;
vs'
,
I
x
v
}}
;
END
)%
proto
.
Lemma
lmerge_spec
{
A
}
(
I
:
A
→
val
→
iProp
Σ
)
(
R
:
A
→
A
→
Prop
)
`
{!
RelDecision
R
,
!
Total
R
}
(
cmp
:
val
)
xs1
xs2
vs1
vs2
:
cmp_spec
I
R
cmp
-
∗
{{{
([
∗
list
]
x
;
v
∈
xs1
;
vs1
,
I
x
v
)
∗
([
∗
list
]
x
;
v
∈
xs2
;
vs2
,
I
x
v
)
}}}
lmerge
cmp
(
val_encode
vs1
)
(
val_encode
vs2
)
{{{
ws
,
RET
val_encode
ws
;
[
∗
list
]
x
;
v
∈
list_merge
R
xs1
xs2
;
ws
,
I
x
v
}}}.
lmerge
cmp
(
llist
vs1
)
(
llist
vs2
)
{{{
ws
,
RET
llist
ws
;
[
∗
list
]
x
;
v
∈
list_merge
R
xs1
xs2
;
ws
,
I
x
v
}}}.
Proof
.
iIntros
"#Hcmp"
(
Ψ
)
"!> [HI1 HI2] HΨ"
.
iL
ö
b
as
"IH"
forall
(
xs1
xs2
vs1
vs2
Ψ
).
wp_lam
.
wp_apply
(
lisnil_spec
(
A
:
=
val
)
with
"[//]"
)
;
iIntros
(
_
).
wp_lam
.
wp_apply
(
lisnil_spec
with
"[//]"
)
;
iIntros
(
_
).
destruct
xs1
as
[|
x1
xs1
],
vs1
as
[|
v1
vs1
]
;
simpl
;
done
||
wp_pures
.
{
iApply
"HΨ"
.
by
rewrite
list_merge_nil_l
.
}
wp_apply
(
lisnil_spec
(
A
:
=
val
)
with
"[//]"
)
;
iIntros
(
_
).
wp_apply
(
lisnil_spec
with
"[//]"
)
;
iIntros
(
_
).
destruct
xs2
as
[|
x2
xs2
],
vs2
as
[|
v2
vs2
]
;
simpl
;
done
||
wp_pures
.
{
iApply
"HΨ"
.
iFrame
.
}
wp_apply
(
lhead_spec
(
A
:
=
val
)
with
"[//]"
)
;
iIntros
(
_
).
wp_apply
(
lhead_spec
(
A
:
=
val
)
with
"[//]"
)
;
iIntros
(
_
).
wp_apply
(
lhead_spec
with
"[//]"
)
;
iIntros
(
_
).
wp_apply
(
lhead_spec
with
"[//]"
)
;
iIntros
(
_
).
iDestruct
"HI1"
as
"[HI1 HI1']"
;
iDestruct
"HI2"
as
"[HI2 HI2']"
.
wp_apply
(
"Hcmp"
with
"[$HI1 $HI2]"
)
;
iIntros
"[HI1 HI2]"
.
case_bool_decide
;
wp_pures
.
-
rewrite
decide_True
//.
wp_apply
(
ltail_spec
(
A
:
=
val
)
with
"[//]"
)
;
iIntros
(
_
).
wp_apply
(
ltail_spec
with
"[//]"
)
;
iIntros
(
_
).
wp_apply
(
"IH"
$!
_
(
x2
::
_
)
with
"HI1'[HI2 HI2']"
)
;
[
simpl
;
iFrame
|].
iIntros
(
ws
)
"HI"
.
wp_apply
(
lcons_spec
(
A
:
=
val
)
with
"[//]"
)
;
iIntros
(
_
).
wp_apply
(
lcons_spec
with
"[//]"
)
;
iIntros
(
_
).
iApply
"HΨ"
.
iFrame
.
-
rewrite
decide_False
//.
wp_apply
(
ltail_spec
(
A
:
=
val
)
with
"[//]"
)
;
iIntros
(
_
).
wp_apply
(
ltail_spec
with
"[//]"
)
;
iIntros
(
_
).
wp_apply
(
"IH"
$!
(
x1
::
_
)
with
"[HI1 HI1'] HI2'"
)
;
[
simpl
;
iFrame
|].
iIntros
(
ws
)
"HI"
.
wp_apply
(
lcons_spec
(
A
:
=
val
)
with
"[//]"
)
;
iIntros
(
_
).
wp_apply
(
lcons_spec
with
"[//]"
)
;
iIntros
(
_
).
iApply
"HΨ"
.
iFrame
.
Qed
.
...
...
@@ -91,13 +91,13 @@ Section sort.
wp_lam
.
wp_recv
(
A
I
R
??
cmp
)
as
"#Hcmp"
.
wp_recv
(
xs
l
vs
)
as
"[Hl HI]"
.
wp_load
.
wp_apply
(
llength_spec
(
A
:
=
val
)
with
"[//]"
)
;
iIntros
(
_
).
wp_load
.
wp_apply
(
llength_spec
with
"[//]"
)
;
iIntros
(
_
).
iDestruct
(
big_sepL2_length
with
"HI"
)
as
%<-.
wp_op
;
case_bool_decide
as
Hlen
;
wp_if
.
{
assert
(
Sorted
R
xs
).
{
destruct
xs
as
[|
x1
[|
x2
xs
]]
;
simpl
in
*
;
eauto
with
lia
.
}
wp_send
with
"[$Hl $HI]"
;
first
by
auto
.
by
iApply
"HΨ"
.
}
wp_load
.
wp_apply
(
lsplit_spec
(
A
:
=
val
)
with
"[//]"
)
;
iIntros
(
vs1
vs2
<
-).
wp_load
.
wp_apply
(
lsplit_spec
with
"[//]"
)
;
iIntros
(
vs1
vs2
-
>
).
wp_alloc
l1
as
"Hl1"
;
wp_alloc
l2
as
"Hl2"
.
iDestruct
(
big_sepL2_app_inv_r
with
"HI"
)
as
(
xs1
xs2
->)
"[HI1 HI2]"
.
wp_apply
(
start_chan_proto_spec
N
sort_protocol
)
;
iIntros
(
cy
)
"Hcy"
.
...
...
@@ -125,10 +125,10 @@ Section sort.
Lemma
sort_client_spec
{
A
}
(
I
:
A
→
val
→
iProp
Σ
)
R
`
{!
RelDecision
R
,
!
Total
R
}
cmp
l
(
vs
:
list
val
)
(
xs
:
list
A
)
:
cmp_spec
I
R
cmp
-
∗
{{{
l
↦
val_encode
vs
∗
[
∗
list
]
x
;
v
∈
xs
;
vs
,
I
x
v
}}}
{{{
l
↦
llist
vs
∗
[
∗
list
]
x
;
v
∈
xs
;
vs
,
I
x
v
}}}
sort_client
cmp
#
l
{{{
ys
ws
,
RET
#()
;
⌜
Sorted
R
ys
⌝
∗
⌜
ys
≡
ₚ
xs
⌝
∗
l
↦
val_encode
ws
∗
[
∗
list
]
y
;
w
∈
ys
;
ws
,
I
y
w
}}}.
l
↦
llist
ws
∗
[
∗
list
]
y
;
w
∈
ys
;
ws
,
I
y
w
}}}.
Proof
.
iIntros
"#Hcmp !>"
(
Φ
)
"Hl HΦ"
.
wp_lam
.
wp_apply
(
start_chan_proto_spec
N
sort_protocol
)
;
iIntros
(
c
)
"Hc"
.
...
...
theories/examples/sort_client.v
View file @
f5e2db76
...
...
@@ -7,27 +7,21 @@ From osiris.examples Require Import sort.
Section
sort_client
.
Context
`
{!
heapG
Σ
,
!
proto_chanG
Σ
}
(
N
:
namespace
).
Local
Arguments
val_encode
_
_
!
_
/.
Lemma
sort_client_le_spec
l
(
xs
:
list
Z
)
:
{{{
l
↦
val_encode
xs
}}}
{{{
l
↦
llist
(
LitV
∘
LitInt
<$>
xs
)
}}}
sort_client
cmpZ
#
l
{{{
ys
,
RET
#()
;
⌜
Sorted
(
≤
)
ys
⌝
∗
⌜
ys
≡
ₚ
xs
⌝
∗
l
↦
val_encode
ys
}}}.
{{{
ys
,
RET
#()
;
⌜
Sorted
(
≤
)
ys
⌝
∗
⌜
ys
≡
ₚ
xs
⌝
∗
l
↦
llist
(
LitV
∘
LitInt
<$>
ys
)
}}}.
Proof
.
assert
(
∀
zs
:
list
Z
,
val_encode
zs
=
val_encode
(
LitV
∘
LitInt
<$>
zs
))
as
Henc
.
{
intros
zs
.
induction
zs
;
f_equal
/=
;
auto
with
f_equal
.
}
iIntros
(
Φ
)
"Hl HΦ"
.
iApply
(
sort_client_spec
N
IZ
(
≤
)
_
_
(
LitV
∘
LitInt
<$>
xs
)
xs
with
"[] [Hl] [HΦ]"
).
{
iApply
cmpZ_spec
.
}
{
rewrite
-
Henc
.
iFrame
"Hl"
.
iInduction
xs
as
[|
x
xs
]
"IH"
;
csimpl
;
first
by
iFrame
.
by
iFrame
"IH"
.
}
{
iFrame
"Hl"
.
iInduction
xs
as
[|
x
xs
]
"IH"
;
csimpl
;
by
iFrame
"#"
.
}
iIntros
"!>"
(
ys
ws
)
"(?&?&?&HI)"
.
iAssert
⌜
ws
=
(
LitV
∘
LitInt
)
<$>
ys
⌝
%
I
with
"[HI]"
as
%->.
{
iInduction
ys
as
[|
y
ys
]
"IH"
forall
(
ws
)
;
destruct
ws
as
[|
w
ws
]
;
csimpl
;
try
done
.
destruct
ws
as
[|
w
ws
]
;
csimpl
;
try
done
.
iDestruct
"HI"
as
"[-> HI2]"
.
by
iDestruct
(
"IH"
with
"HI2"
)
as
%->.
}
rewrite
-
Henc
.
iApply
(
"HΦ"
$!
ys
with
"[$]"
).
iApply
(
"HΦ"
$!
ys
with
"[$]"
).
Qed
.
End
sort_client
.
theories/examples/sort_elem_client.v
View file @
f5e2db76
...
...
@@ -31,7 +31,7 @@ Section sort_elem_client.
Lemma
send_all_spec
c
p
xs'
xs
vs
:
{{{
c
↣
sort_elem_head_protocol
I
R
xs'
<++>
p
@
N
∗
[
∗
list
]
x
;
v
∈
xs
;
vs
,
I
x
v
}}}
send_all
c
(
val_encode
vs
)
send_all
c
(
llist
vs
)
{{{
RET
#()
;
c
↣
sort_elem_tail_protocol
I
R
(
xs'
++
xs
)
[]
<++>
p
@
N
}}}.
Proof
.
iIntros
(
Φ
)
"[Hc HI] HΦ"
.
...
...
@@ -46,7 +46,7 @@ Section sort_elem_client.
Sorted
R
ys'
→
{{{
c
↣
sort_elem_tail_protocol
I
R
xs
ys'
<++>
p
@
N
}}}
recv_all
c
{{{
ys
ws
,
RET
(
val_encode
ws
)
;
{{{
ys
ws
,
RET
(
llist
ws
)
;
⌜
Sorted
R
(
ys'
++
ys
)
⌝
∗
⌜
ys'
++
ys
≡
ₚ
xs
⌝
∗
c
↣
p
@
N
∗
[
∗
list
]
y
;
w
∈
ys
;
ws
,
I
y
w
}}}.
...
...
@@ -57,7 +57,7 @@ Section sort_elem_client.
-
wp_recv
(
y
v
)
as
(
Htl
)
"HIxv"
.
wp_apply
(
"IH"
with
"[] Hc"
)
;
first
by
auto
using
Sorted_snoc
.
iIntros
(
ys
ws
).
rewrite
-!
assoc_L
.
iDestruct
1
as
(??)
"[Hc HI]"
.
wp_apply
(
lcons_spec
(
A
:
=
val
)
with
"[//]"
)
;
iIntros
(
_
).
wp_apply
(
lcons_spec
with
"[//]"
)
;
iIntros
(
_
).
iApply
(
"HΦ"
$!
(
y
::
ys
)).
simpl
;
iFrame
;
auto
.
-
wp_apply
(
lnil_spec
with
"[//]"
)
;
iIntros
(
_
).
iApply
(
"HΦ"
$!
[]
[])
;
rewrite
/=
right_id_L
;
by
iFrame
.
...
...
@@ -66,8 +66,8 @@ Section sort_elem_client.
Lemma
sort_client_spec
cmp
vs
xs
:
cmp_spec
I
R
cmp
-
∗
{{{
[
∗
list
]
x
;
v
∈
xs
;
vs
,
I
x
v
}}}
sort_elem_client
cmp
(
val_encode
vs
)
{{{
ys
ws
,
RET
(
val_encode
ws
)
;
⌜
Sorted
R
ys
⌝
∗
⌜
ys
≡
ₚ
xs
⌝
∗
sort_elem_client
cmp
(
llist
vs
)
{{{
ys
ws
,
RET
(
llist
ws
)
;
⌜
Sorted
R
ys
⌝
∗
⌜
ys
≡
ₚ
xs
⌝
∗
[
∗
list
]
y
;
w
∈
ys
;
ws
,
I
y
w
}}}.
Proof
.
iIntros
"#Hcmp !>"
(
Φ
)
"HI HΦ"
.
wp_lam
.
...
...
theories/utils/list.v
View file @
f5e2db76
From
iris
.
heap_lang
Require
Export
proofmode
notation
.
From
iris
.
heap_lang
Require
Import
assert
.
From
osiris
.
utils
Require
Export
encodable
.
(** Immutable ML-style functional lists *)
Instance
list_val_enc
`
{
ValEnc
A
}
:
ValEnc
(
list
A
)
:
=
fix
go
xs
:
=
let
_
:
ValEnc
_
:
=
@
go
in
match
xs
with
|
[]
=>
val_encode
None
|
x
::
xs
=>
val_encode
(
Some
(
x
,
xs
))
end
.
Fixpoint
llist
(
vs
:
list
val
)
:
val
:
=
match
vs
with
|
[]
=>
NONEV
|
v
::
vs
=>
SOMEV
(
v
,
llist
vs
)
end
%
V
.
Arguments
llist
:
simpl
never
.
Definition
lnil
:
val
:
=
λ
:
<>,
NONEV
.
Definition
lcons
:
val
:
=
λ
:
"x"
"l"
,
SOME
(
"x"
,
"l"
).
...
...
@@ -49,15 +47,6 @@ Definition lreplicate : val :=
if
:
"n"
=
#
0
then
lnil
#()
else
let
:
"l"
:
=
"go"
(
"n"
-
#
1
)
"x"
in
lcons
"x"
"l"
.
Definition
llist_member
:
val
:
=
rec
:
"go"
"x"
"l"
:
=
match
:
"l"
with
NONE
=>
#
false
|
SOME
"p"
=>
if
:
Fst
"p"
=
"x"
then
#
true
else
let
:
"l"
:
=
(
Snd
"p"
)
in
"go"
"x"
"l"
end
.
Definition
llength
:
val
:
=
rec
:
"go"
"l"
:
=
match
:
"l"
with
...
...
@@ -97,195 +86,138 @@ Definition lsplit : val :=
λ
:
"l"
,
lsplit_at
"l"
((
llength
"l"
)
`
quot
`
#
2
).
Section
lists
.
Context
`
{
heapG
Σ
}
`
{
ValEncDec
A
}
.
Context
`
{
heapG
Σ
}.
Implicit
Types
i
:
nat
.
Implicit
Types
x
:
A
.
Implicit
Types
x
s
:
list
A
.
Implicit
Types
v
:
val
.
Implicit
Types
v
s
:
list
val
.
Lemma
lnil_spec
:
{{{
True
}}}
lnil
#()
{{{
RET
val_encode
[]
;
True
}}}.
{{{
True
}}}
lnil
#()
{{{
RET
llist
[]
;
True
}}}.
Proof
.
iIntros
(
Φ
_
)
"HΦ"
.
wp_lam
.
by
iApply
"HΦ"
.
Qed
.
Lemma
lcons_spec
x
xs
:
{{{
True
}}}
lcons
(
val_encode
x
)
(
val_encode
xs
)
{{{
RET
val_encode
(
x
::
xs
)
;
True
}}}.
Lemma
lcons_spec
v
vs
:
{{{
True
}}}
lcons
v
(
llist
vs
)
{{{
RET
llist
(
v
::
vs
)
;
True
}}}.
Proof
.
iIntros
(
Φ
_
)
"HΦ"
.
wp_lam
.
wp_pures
.
by
iApply
"HΦ"
.
Qed
.
Lemma
lisnil_spec
x
s
:
Lemma
lisnil_spec
v
s
:
{{{
True
}}}
lisnil
(
val_encode
x
s
)
{{{
RET
#(
if
x
s
is
[]
then
true
else
false
)
;
True
}}}.
Proof
.
iIntros
(
Φ
_
)
"HΦ"
.
wp_lam
.
destruct
x
s
;
wp_pures
;
by
iApply
"HΦ"
.
Qed
.
lisnil
(
llist
v
s
)
{{{
RET
#(
if
v
s
is
[]
then
true
else
false
)
;
True
}}}.
Proof
.
iIntros
(
Φ
_
)
"HΦ"
.
wp_lam
.
destruct
v
s
;
wp_pures
;
by
iApply
"HΦ"
.
Qed
.
Lemma
lhead_spec
x
xs
:
{{{
True
}}}
lhead
(
val_encode
(
x
::
x
s
))
{{{
RET
v
al_encode
x
;
True
}}}.
Lemma
lhead_spec
v
vs
:
{{{
True
}}}
lhead
(
llist
(
v
::
v
s
))
{{{
RET
v
;
True
}}}.
Proof
.
iIntros
(
Φ
_
)
"HΦ"
.
wp_lam
.
wp_pures
.
by
iApply
"HΦ"
.
Qed
.
Lemma
ltail_spec
x
x
s
:
{{{
True
}}}
ltail
(
val_encode
(
x
::
xs
))
{{{
RET
val_encode
x
s
;
True
}}}.
Lemma
ltail_spec
v
v
s
:
{{{
True
}}}
ltail
(
llist
(
v
::
vs
))
{{{
RET
llist
v
s
;
True
}}}.
Proof
.
iIntros
(
Φ
_
)
"HΦ"
.
wp_lam
.
wp_pures
.
by
iApply
"HΦ"
.
Qed
.
Lemma
llookup_spec
i
xs
x
:
xs
!!
i
=
Some
x
→
{{{
True
}}}
llookup
#
i
(
val_encode
xs
)
{{{
RET
val_encode
x
;
True
}}}.
Lemma
llookup_spec
i
vs
v
:
vs
!!
i
=
Some
v
→
{{{
True
}}}
llookup
#
i
(
llist
vs
)
{{{
RET
v
;
True
}}}.
Proof
.
iIntros
(
Hi
Φ
Hl
)
"HΦ"
.
iInduction
x
s
as
[|
x
'
x
s
]
"IH"
forall
(
i
Hi
Hl
)
;
iIntros
(
Hi
Φ
_
)
"HΦ"
.
iInduction
v
s
as
[|
v
'
v
s
]
"IH"
forall
(
i
Hi
)
;
destruct
i
as
[|
i
]=>
//
;
simplify_eq
/=.
{
wp_lam
.
wp_pures
.
by
iApply
(
lhead_spec
with
"[//]"
).
}
wp_lam
.
wp_pures
.
wp_apply
(
ltail_spec
with
"[//]"
)
;
iIntros
(
?
).
wp_let
.
wp_apply
(
ltail_spec
with
"[//]"
)
;
iIntros
(
_
).
wp_let
.
wp_op
.
rewrite
Nat2Z
.
inj_succ
-
Z
.
add_1_l
Z
.
add_simpl_l
.
by
iApply
"IH"
.
Qed
.
Lemma
linsert_spec
i
xs
x
:
is_Some
(
xs
!!
i
)
→
{{{
True
}}}
linsert
#
i
(
val_encode
x
)
(
val_encode
xs
)
{{{
RET
val_encode
(<[
i
:
=
x
]>
xs
)
;
True
}}}.
Lemma
linsert_spec
i
vs
v
:
is_Some
(
vs
!!
i
)
→
{{{
True
}}}
linsert
#
i
v
(
llist
vs
)
{{{
RET
llist
(<[
i
:
=
v
]>
vs
)
;
True
}}}.
Proof
.
iIntros
([
w
Hi
]
Φ
Hl
)
"HΦ"
.
iInduction
x
s
as
[|
x
'
x
s
]
"IH"
forall
(
i
Hi
Hl
Φ
)
;
iIntros
([
w
Hi
]
Φ
_
)
"HΦ"
.
iInduction
v
s
as
[|
v
'
v
s
]
"IH"
forall
(
i
Hi
Φ
)
;
destruct
i
as
[|
i
]=>
//
;
simplify_eq
/=.
{
wp_lam
.
wp_pures
.
wp_apply
(
ltail_spec
with
"[//]"
)
.
iIntros
(
?
).
{
wp_lam
.
wp_pures
.
wp_apply
(
ltail_spec
with
"[//]"
)
;
iIntros
(
_
).
wp_let
.
by
iApply
(
lcons_spec
with
"[//]"
).
}
wp_lam
;
wp_pures
.
wp_apply
(
ltail_spec
with
"[//]"
)
;
iIntros
(
?
).
wp_let
.
wp_apply
(
ltail_spec
with
"[//]"
)
;
iIntros
(
_
).
wp_let
.
wp_op
.
rewrite
Nat2Z
.
inj_succ
-
Z
.
add_1_l
Z
.
add_simpl_l
.
wp_apply
(
"IH"
with
"[//]
[//]
"
)
.
iIntros
(
?
).
wp_let
.
wp_apply
(
"IH"
with
"[//]"
)
;
iIntros
(
_
).
wp_apply
(
lhead_spec
with
"[//]"
)
;
iIntros
"_"
.
by
wp_apply
(
lcons_spec
with
"[//]"
).
Qed
.
(*
Lemma llist_member_spec `{EqDecision A} (xs : list A) (x : A) :
{{{ True }}}
llist_member (val_encode x) (val_encode xs)
{{{ RET #(bool_decide (x ∈ xs)); True }}}.
Proof.
iIntros (Φ Hl) "HΦ".
iInduction xs as [|x' xs] "IH" forall (Hl); simplify_eq/=.
{ wp_lam; wp_pures. by iApply "HΦ". }
wp_lam; wp_pures.
destruct (bool_decide_reflect (val_encode x' = val_encode x)); simplify_eq/=; wp_if.
{ rewrite (bool_decide_true (_ ∈ _ :: _)); last by left. by iApply "HΦ". }
wp_proj. wp_let. iApply ("IH" with "[//]").
destruct (bool_decide_reflect (x ∈ xs)).
- by rewrite bool_decide_true; last by right.
- by rewrite bool_decide_false ?elem_of_cons; last naive_solver.
Qed.
*)
Lemma
lreplicate_spec
i
x
:
{{{
True
}}}
lreplicate
#
i
(
val_encode
x
)
{{{
RET
val_encode
(
replicate
i
x
)
;
True
}}}.
Lemma
lreplicate_spec
i
v
:
{{{
True
}}}
lreplicate
#
i
v
{{{
RET
llist
(
replicate
i
v
)
;
True
}}}.
Proof
.
iIntros
(
Φ
_
)
"HΦ"
.
iInduction
i
as
[|
i
]
"IH"
forall
(
Φ
)
;
simpl
.
{
wp_lam
;
wp_pures
.
iApply
(
lnil_spec
with
"[//]"
).
iApply
"HΦ"
.
}
{
wp_lam
;
wp_pures
.
iApply
(
lnil_spec
with
"[//]"
)
;
auto
.
}
wp_lam
;
wp_pures
.
rewrite
Nat2Z
.
inj_succ
-
Z
.
add_1_l
Z
.
add_simpl_l
.
wp_apply
"IH"
;
iIntros
(
Hl
).
wp_let
.
by
iApply
(
lcons_spec
with
"[//]"
).
wp_apply
"IH"
;
iIntros
(
_
).
wp_let
.
by
iApply
(
lcons_spec
with
"[//]"
).
Qed
.
Lemma
llength_spec
x
s
:
{{{
True
}}}
llength
(
val_encode
x
s
)
{{{
RET
#(
length
x
s
)
;
True
}}}.
Lemma
llength_spec
v
s
:
{{{
True
}}}
llength
(
llist
v
s
)
{{{
RET
#(
length
v
s
)
;
True
}}}.
Proof
.
iIntros
(
Φ
Hl
)
"HΦ"
.
iInduction
x
s
as
[|
x
'
x
s
]
"IH"
forall
(
Hl
Φ
)
;
simplify_eq
/=.
iIntros
(
Φ
_
)
"HΦ"
.
iInduction
v
s
as
[|
v
'
v
s
]
"IH"
forall
(
Φ
)
;
simplify_eq
/=.
{
wp_lam
.
wp_match
.
by
iApply
"HΦ"
.
}
wp_lam
.
wp_match
.
wp_proj
.
wp_apply
(
"IH"
with
"[//]"
)
;
iIntros
"_ /="
.
wp_op
.
wp_apply
"IH"
;
iIntros
"_ /="
.
wp_op
.
rewrite
(
Nat2Z
.
inj_add
1
).
by
iApply
"HΦ"
.
Qed
.
Lemma
lsnoc_spec
xs
x
:
{{{
True
}}}
lsnoc
(
val_encode
xs
)
(
val_encode
x
)
{{{
RET
(
val_encode
(
xs
++[
x
]))
;
True
}}}.
Lemma
lsnoc_spec
vs
v
:
{{{
True
}}}
lsnoc
(
llist
vs
)
v
{{{
RET
(
llist
(
vs
++
[
v
]))
;
True
}}}.
Proof
.
iIntros
(
Φ
_
)
"HΦ"
.
iInduction
x
s
as
[|
x
'
x
s
]
"IH"
forall
(
Φ
).
iInduction
v
s
as
[|
v
'
v
s
]
"IH"
forall
(
Φ
).
{
wp_rec
.
wp_pures
.
wp_lam
.
wp_pures
.
by
iApply
"HΦ"
.
}
wp_rec
.
wp_apply
"IH"
=>
//.
iIntros
(
_
).
by
wp_apply
lcons_spec
=>
//.
wp_rec
.
wp_apply
"IH"
;
iIntros
(
_
).
by
wp_apply
lcons_spec
=>
//.
Qed
.
Lemma
ltake_spec
xs
(
n
:
Z
)
:
{{{
True
}}}
ltake
(
val_encode
xs
)
#
n
{{{
RET
val_encode
(
take
(
Z
.
to_nat
n
)
xs
)
;
True
}}}.
Lemma
ltake_spec
vs
(
n
:
nat
)
:
{{{
True
}}}
ltake
(
llist
vs
)
#
n
{{{
RET
llist
(
take
n
vs
)
;
True
}}}.
Proof
.
iIntros
(
Φ
_
)
"HΦ"
.
iInduction
xs
as
[|
x'
xs
]
"IH"
forall
(
n
Φ
).
-
wp_rec
.
wp_pures
.
destruct
(
bool_decide
(
n
≤
0
))
;
wp_pures
;
rewrite
take_nil
;
by
iApply
"HΦ"
.
iInduction
vs
as
[|
x'
vs
]
"IH"
forall
(
n
Φ
).
-
wp_rec
.
wp_pures
.
destruct
(
decide
(
n
≤
0
)).
+
rewrite
bool_decide_true
=>
//.
wp_pures
.
rewrite
Z_to_nat_nonpos
=>
//.
rewrite
firstn_O
.
by
iApply
"HΦ"
.
+
rewrite
bool_decide_false
=>
//.
wp_apply
(
"IH"
)
;
iIntros
(
_
).
wp_apply
(
lcons_spec
)=>
//
;
iIntros
(
_
).
rewrite
-
firstn_cons
.
rewrite
-
Z2Nat
.
inj_succ
;
last
lia
.
rewrite
Z
.
succ_pred
.
by
iApply
"HΦ"
.
destruct
(
bool_decide
(
n
≤
0
))
;
wp_pures
;
rewrite
take_nil
;
by
iApply
"HΦ"
.
-
wp_rec
;
destruct
n
as
[|
n
]
;
wp_pures
;
first
by
iApply
"HΦ"
.
rewrite
Nat2Z
.
inj_succ
Z
.
sub_1_r
Z
.
pred_succ
.
wp_apply
"IH"
;
iIntros
(
_
).
wp_apply
(
lcons_spec
with
"[//]"
)
;
iIntros
(
_
).
by
iApply
"HΦ"
.
Qed
.
Lemma
ldrop_spec
xs
(
n
:
Z
)
:
{{{
True
}}}
ldrop
(
val_encode
xs
)
#
n
{{{
RET
val_encode
(
drop
(
Z
.
to_nat
n
)
xs
)
;
True
}}}.
Lemma
ldrop_spec
vs
(
n
:
nat
)
:
{{{
True
}}}
ldrop
(
llist
vs
)
#
n
{{{
RET
llist
(
drop
n
vs
)
;
True
}}}.
Proof
.
iIntros
(
Φ
_
)
"HΦ"
.
iInduction
xs
as
[|
x'
xs
]
"IH"
forall
(
n
Φ
).
-
wp_rec
.
wp_pures
.
destruct
(
bool_decide
(
n
≤
0
))
;
wp_pures
;
rewrite
drop_nil
;
by
iApply
"HΦ"
.
iInduction
vs
as
[|
x'
vs
]
"IH"
forall
(
n
Φ
).
-
wp_rec
.
wp_pures
.
destruct
(
decide
(
n
≤
0
)).
+
rewrite
bool_decide_true
=>
//.
wp_pures
.
rewrite
Z_to_nat_nonpos
=>
//.
rewrite
drop_0
.
by
iApply
"HΦ"
.
+
rewrite
bool_decide_false
=>
//.
wp_apply
"IH"
;
iIntros
(
_
).
rewrite
-{
1
}(
Z
.
succ_pred
n
)
Z2Nat
.
inj_succ
/=
-
Z
.
sub_1_r
;
last
lia
.
by
iApply
"HΦ"
.
destruct
(
bool_decide
(
n
≤
0
))
;
wp_pures
;
rewrite
drop_nil
;
by
iApply
"HΦ"
.
-
wp_rec
;
destruct
n
as
[|
n
]
;
wp_pures
;
first
by
iApply
"HΦ"
.
rewrite
Nat2Z
.
inj_succ
Z
.
sub_1_r
Z
.
pred_succ
.
wp_apply
"IH"
;
iIntros
(
_
).
by
iApply
"HΦ"
.
Qed
.