Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
Actris
Commits
1fa2c070
Commit
1fa2c070
authored
Jul 04, 2019
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Some renaming.
parent
8bf5d63b
Changes
8
Hide whitespace changes
Inline
Side-by-side
Showing
8 changed files
with
150 additions
and
145 deletions
+150
-145
_CoqProject
_CoqProject
+4
-4
theories/examples/loop_sort.v
theories/examples/loop_sort.v
+3
-3
theories/examples/mapper.v
theories/examples/mapper.v
+1
-1
theories/examples/producer_consumer.v
theories/examples/producer_consumer.v
+48
-50
theories/examples/sort.v
theories/examples/sort.v
+10
-10
theories/examples/sort_client.v
theories/examples/sort_client.v
+6
-6
theories/examples/sort_elem.v
theories/examples/sort_elem.v
+65
-58
theories/examples/sort_elem_client.v
theories/examples/sort_elem_client.v
+13
-13
No files found.
_CoqProject
View file @
1fa2c070
...
...
@@ -10,8 +10,8 @@ theories/channel/channel.v
theories/channel/proto_model.v
theories/channel/proto_channel.v
theories/channel/proofmode.v
theories/examples/
list_
sort.v
theories/examples/
list_sort_instances
.v
theories/examples/
list_
sort_elem.v
theories/examples/sort.v
theories/examples/
sort_client
.v
theories/examples/sort_elem.v
theories/examples/loop_sort.v
theories/examples/
list_
sort_elem_client.v
theories/examples/sort_elem_client.v
theories/examples/loop_sort.v
View file @
1fa2c070
...
...
@@ -2,11 +2,11 @@ From stdpp Require Import sorting.
From
osiris
.
channel
Require
Import
proto_channel
.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
From
osiris
.
utils
Require
Import
list
.
From
osiris
.
examples
Require
Import
list_
sort
.
From
osiris
.
examples
Require
Import
sort
.
Definition
loop_sort_service
:
val
:
=
rec
:
"go"
"c"
:
=
if
:
recv
"c"
then
list_
sort_service
"c"
;;
"go"
"c"
if
:
recv
"c"
then
sort_service
"c"
;;
"go"
"c"
else
if
:
recv
"c"
then
let
:
"d"
:
=
start_chan
"go"
in
send
"c"
"d"
;;
...
...
@@ -33,7 +33,7 @@ Section loop_sort.
Proof
.
iIntros
(
Ψ
)
"Hc HΨ"
.
iL
ö
b
as
"IH"
forall
(
c
Ψ
).
wp_rec
.
wp_apply
(
branch_spec
with
"Hc"
)
;
iIntros
([])
"/= [Hc _]"
;
wp_if
.
{
wp_apply
(
list_
sort_service_spec
with
"Hc"
)
;
iIntros
"Hc"
.
{
wp_apply
(
sort_service_spec
with
"Hc"
)
;
iIntros
"Hc"
.
by
wp_apply
(
"IH"
with
"Hc"
).
}
wp_apply
(
branch_spec
with
"Hc"
)
;
iIntros
([])
"/= [Hc _]"
;
wp_if
.
-
wp_apply
(
start_chan_proto_spec
N
loop_sort_protocol
)
;
iIntros
(
d
)
"Hd"
.
...
...
theories/examples/mapper.v
View file @
1fa2c070
...
...
@@ -3,7 +3,7 @@ From osiris.channel Require Import proto_channel proofmode.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
From
iris
.
heap_lang
Require
Import
assert
.
From
osiris
.
utils
Require
Import
list
compare
spin_lock
contribution
.
From
osiris
.
examples
Require
Import
list_
sort_elem
.
From
osiris
.
examples
Require
Import
sort_elem
.
From
iris
.
algebra
Require
Import
gmultiset
.
Definition
mapper
:
val
:
=
...
...
theories/examples/producer_consumer.v
View file @
1fa2c070
...
...
@@ -2,9 +2,7 @@ From stdpp Require Import sorting.
From
osiris
.
channel
Require
Import
proto_channel
proofmode
.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
From
iris
.
heap_lang
Require
Import
assert
.
From
iris
.
heap_lang
.
lib
Require
Import
spin_lock
.
From
osiris
.
utils
Require
Import
list
compare
.
From
osiris
.
utils
Require
Import
list
compare
spin_lock
.
Definition
qnew
:
val
:
=
λ
:
<>,
#().
Definition
qenqueue
:
val
:
=
λ
:
"q"
"v"
,
#().
...
...
@@ -20,55 +18,55 @@ Definition stop := false.
Definition
some
:
=
true
.
Definition
none
:
=
false
.
Definition
dist_queue
:
val
:
=
Definition
pd_loop
:
val
:
=
rec
:
"go"
"q"
"pc"
"cc"
"c"
:
=
if
:
"cc"
≤
#
0
then
#()
else
if
:
recv
"c"
(* enq/deq *)
then
if
:
recv
"c"
(* cont/stop *)
then
"go"
(
qenqueue
"q"
(
recv
"c"
))
"pc"
"cc"
"c"
else
"go"
"q"
(
"pc"
-#
1
)
"cc"
"c"
else
if
:
(
qis_empty
"q"
)
then
if
:
"pc"
≤
#
0
then
send
"c"
#
stop
;;
"go"
"q"
"pc"
(
"cc"
-#
1
)
"c"
else
send
"c"
#
cont
;;
send
"c"
#
none
;;
"go"
"q"
"pc"
"cc"
"c"
else
send
"
c
"
#
cont
;;
send
"c"
#
some
;;
let
:
"qv"
:
=
qdequeue
"q"
in
send
"c"
(
Snd
"qv"
)
;;
"go"
(
Fst
"qv"
)
"pc"
"cc"
"c"
.
Definition
producer
:
val
:
=
rec
:
"go"
"c"
"
l
"
"produce"
:
=
(* acquire "l";; *)
match
:
"produce"
#()
with
SOME
"v"
=>
acquire
"l"
;;
send
"c"
#
enq
;;
send
"c"
#
cont
;;
send
"c"
"
v"
;;
release
"l"
;;
"go
"
"c"
"
l
"
"
produce"
|
NONE
=>
acquire
"l"
;;
send
"c"
#
enq
;;
send
"c"
#
stop
release
"l"
end
.
Definition
consumer
:
val
:
=
rec
:
"go"
"c"
"l"
"consume"
:
=
acquire
"l"
;;
send
"c"
#
deq
;;
if
:
recv
"c"
(* cont/
stop
*)
then
if
:
recv
"c"
(* some/none *)
then
let
:
"v"
:
=
SOME
(
recv
"c"
)
in
release
"l"
;;
"consume"
"v"
;;
"go"
"c"
"l"
"consume"
(* "consume" "v";; release "l";; "go" "c" "l" "consume" *)
else
release
"l"
;;
"go"
"c"
"l"
"consume"
else
"consume"
NONE
;;
release
"l"
;;
#().
(* else release
"l"
;; "consume" NONE;; #().
*)
(* Makes n producers and m consumers *)
Definition
produce_consume
:
val
:
=
λ
:
"produce"
"consume
"
"
p
c"
"
cc"
,
#()
.
Section
list_
sort_elem
.
if
:
recv
"c"
then
(* enq/deq *)
if
:
recv
"c"
then
(* cont/stop *)
"go"
(
qenqueue
"q"
(
recv
"c"
))
"pc"
"cc"
"c"
else
"go"
"q"
(
"pc"
-#
1
)
"cc"
"c"
else
if
:
(
qis_empty
"q"
)
then
if
:
"pc"
≤
#
0
then
send
"c"
#
stop
;;
"go"
"
q
"
"pc"
(
"cc"
-#
1
)
"c"
else
send
"c"
#
cont
;;
send
"c"
#
none
;;
"go"
"q"
"pc"
"cc"
"c"
else
send
"c"
#
cont
;;
send
"
c
"
#
some
;;
let
:
"qv"
:
=
qdequeue
"q"
in
send
"c"
(
Snd
"qv"
)
;;
"go"
(
Fst
"
q
v"
)
"pc"
"cc"
"c"
.
Definition
new_pd
:
val
:
=
λ
:
"
p
c"
"
cc"
,
let
:
"q"
:
=
qnew
#()
in
let
:
"c"
:
=
start_chan
(
λ
:
"c"
,
pd_loop
"q
"
"
p
c"
"
cc
"
"
c"
)
in
let
:
"l"
:
=
new_lock
#()
in
(
"c"
,
"l"
).
Definition
pd_send
:
val
:
=
λ
:
"cl"
"x"
,
acquire
(
Snd
"cl"
)
;;
send
(
Fst
"cl"
)
#
enq
;;
send
(
Fst
"cl"
)
#
cont
;;
send
(
Fst
"cl"
)
"x"
;;
release
(
Snd
"cl"
).
Definition
pd_stop
:
val
:
=
λ
:
"
c
l"
,
acquire
(
Fst
"cl"
)
;;
send
(
Snd
"cl"
)
#
enq
;;
send
(
Snd
"cl"
)
#
stop
;;
release
(
Fst
"cl"
).
Definition
pd_recv
:
val
:
=
rec
:
"go"
"cl"
:
=
acquire
(
Fst
"
c
l"
)
;;
send
(
Snd
"
c
l"
)
#
deq
;;
if
:
recv
(
Snd
"
c
l"
)
then
(* cont/stop
*)
if
:
recv
(
Snd
"cl"
)
then
(* some/none *)
let
:
"v"
:
=
recv
(
Snd
"cl"
)
in
release
(
Fst
"cl"
)
;;
SOME
"v"
else
release
(
Fst
"cl"
)
;;
"go
"
"c"
"
l"
else
release
(
Fst
"cl"
)
;;
NONE
.
Section
sort_elem
.
Context
`
{!
heapG
Σ
,
!
proto_chanG
Σ
}
(
N
:
namespace
).
Definition
queue_prot
:
iProto
Σ
:
=
(
END
)%
proto
.
...
...
theories/examples/
list_
sort.v
→
theories/examples/sort.v
View file @
1fa2c070
...
...
@@ -13,7 +13,7 @@ Definition lmerge : val :=
then
lcons
"y"
(
"go"
"cmp"
(
ltail
"ys"
)
"zs"
)
else
lcons
"z"
(
"go"
"cmp"
"ys"
(
ltail
"zs"
)).
Definition
list_
sort_service
:
val
:
=
Definition
sort_service
:
val
:
=
rec
:
"go"
"c"
:
=
let
:
"cmp"
:
=
recv
"c"
in
let
:
"xs"
:
=
recv
"c"
in
...
...
@@ -30,12 +30,12 @@ Definition list_sort_service : val :=
"xs"
<-
lmerge
"cmp"
!
"ys"
!
"zs"
;;
send
"c"
#().
Definition
list_
sort_client
:
val
:
=
λ
:
"cmp"
"xs"
,
let
:
"c"
:
=
start_chan
list_
sort_service
in
Definition
sort_client
:
val
:
=
λ
:
"cmp"
"xs"
,
let
:
"c"
:
=
start_chan
sort_service
in
send
"c"
"cmp"
;;
send
"c"
"xs"
;;
recv
"c"
.
Section
list_
sort
.
Section
sort
.
Context
`
{!
heapG
Σ
,
!
proto_chanG
Σ
}
(
N
:
namespace
).
Definition
sort_protocol
:
iProto
Σ
:
=
...
...
@@ -82,9 +82,9 @@ Section list_sort.
iApply
"HΨ"
.
iFrame
.
Qed
.
Lemma
list_
sort_service_spec
p
c
:
Lemma
sort_service_spec
p
c
:
{{{
c
↣
iProto_dual
sort_protocol
<++>
p
@
N
}}}
list_
sort_service
c
sort_service
c
{{{
RET
#()
;
c
↣
p
@
N
}}}.
Proof
.
iIntros
(
Ψ
)
"Hc HΨ"
.
iL
ö
b
as
"IH"
forall
(
p
c
Ψ
).
...
...
@@ -122,21 +122,21 @@ Section list_sort.
-
by
iApply
"HΨ"
.
Qed
.
Lemma
list_
sort_client_spec
{
A
}
(
I
:
A
→
val
→
iProp
Σ
)
R
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
}}}
list_
sort_client
cmp
#
l
sort_client
cmp
#
l
{{{
ys
ws
,
RET
#()
;
⌜
Sorted
R
ys
⌝
∗
⌜
ys
≡
ₚ
xs
⌝
∗
l
↦
val_encode
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"
.
{
rewrite
-(
right_id
END
%
proto
_
(
iProto_dual
_
)).
wp_apply
(
list_
sort_service_spec
with
"Hc"
)
;
auto
.
}
wp_apply
(
sort_service_spec
with
"Hc"
)
;
auto
.
}
wp_send
with
"[$Hcmp]"
.
wp_send
with
"[$Hl]"
.
wp_recv
(
ys
ws
)
as
"(Hsorted & Hperm & Hl & HI)"
.
wp_pures
.
iApply
"HΦ"
;
iFrame
.
Qed
.
End
list_
sort
.
End
sort
.
theories/examples/
list_sort_instances
.v
→
theories/examples/
sort_client
.v
View file @
1fa2c070
...
...
@@ -2,22 +2,22 @@ From stdpp Require Import sorting.
From
osiris
.
channel
Require
Import
proto_channel
.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
From
osiris
.
utils
Require
Import
list
compare
.
From
osiris
.
examples
Require
Import
list_
sort
.
From
osiris
.
examples
Require
Import
sort
.
Section
list_sort_instances
.
Section
sort_client
.
Context
`
{!
heapG
Σ
,
!
proto_chanG
Σ
}
(
N
:
namespace
).
Local
Arguments
val_encode
_
_
!
_
/.
Lemma
list_
sort_client_le_spec
l
(
xs
:
list
Z
)
:
Lemma
sort_client_le_spec
l
(
xs
:
list
Z
)
:
{{{
l
↦
val_encode
xs
}}}
list_
sort_client
cmpZ
#
l
sort_client
cmpZ
#
l
{{{
ys
,
RET
#()
;
⌜
Sorted
(
≤
)
ys
⌝
∗
⌜
ys
≡
ₚ
xs
⌝
∗
l
↦
val_encode
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
(
list_
sort_client_spec
N
IZ
(
≤
)
_
_
(
LitV
∘
LitInt
<$>
xs
)
xs
with
"[] [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
.
...
...
@@ -30,4 +30,4 @@ Section list_sort_instances.
by
iDestruct
(
"IH"
with
"HI2"
)
as
%->.
}
rewrite
-
Henc
.
iApply
(
"HΦ"
$!
ys
with
"[$]"
).
Qed
.
End
list_sort_instances
.
End
sort_client
.
theories/examples/
list_
sort_elem.v
→
theories/examples/sort_elem.v
View file @
1fa2c070
...
...
@@ -7,25 +7,25 @@ From osiris.utils Require Import list compare.
Definition
cont
:
=
true
.
Definition
stop
:
=
false
.
Definition
list_
sort_elem_service_split
:
val
:
=
Definition
sort_elem_service_split
:
val
:
=
rec
:
"go"
"c"
"c1"
"c2"
:
=
if
:
~(
recv
"c"
)
then
send
"c1"
#
stop
;;
send
"c2"
#
stop
else
let
:
"x"
:
=
recv
"c"
in
send
"c1"
#
cont
;;
send
"c1"
"x"
;;
"go"
"c"
"c2"
"c1"
.
Definition
list_
sort_elem_service_move
:
val
:
=
Definition
sort_elem_service_move
:
val
:
=
rec
:
"go"
"c"
"cin"
:
=
if
:
~(
recv
"cin"
)
then
send
"c"
#
stop
else
let
:
"x"
:
=
recv
"cin"
in
send
"c"
#
cont
;;
send
"c"
"x"
;;
"go"
"c"
"cin"
.
Definition
list_
sort_elem_service_merge
:
val
:
=
Definition
sort_elem_service_merge
:
val
:
=
rec
:
"go"
"cmp"
"c"
"x1"
"c1"
"c2"
:
=
if
:
~recv
"c2"
then
send
"c"
#
cont
;;
send
"c"
"x1"
;;
list_
sort_elem_service_move
"c"
"c1"
sort_elem_service_move
"c"
"c1"
else
let
:
"x2"
:
=
recv
"c2"
in
if
:
"cmp"
"x1"
"x2"
then
...
...
@@ -33,7 +33,7 @@ Definition list_sort_elem_service_merge : val :=
else
send
"c"
#
cont
;;
send
"c"
"x2"
;;
"go"
"cmp"
"c"
"x1"
"c1"
"c2"
.
Definition
list_
sort_elem_service
:
val
:
=
Definition
sort_elem_service
:
val
:
=
rec
:
"go"
"cmp"
"c"
:
=
if
:
~(
recv
"c"
)
then
send
"c"
#
stop
else
let
:
"x"
:
=
recv
"c"
in
...
...
@@ -45,59 +45,65 @@ Definition list_sort_elem_service : val :=
let
:
"c2"
:
=
Fst
"cc2"
in
let
:
"c2'"
:
=
Snd
"cc2"
in
send
"c1"
#
cont
;;
send
"c1"
"x"
;;
send
"c2"
#
cont
;;
send
"c2"
"y"
;;
list_
sort_elem_service_split
"c"
"c1"
"c2"
;;
sort_elem_service_split
"c"
"c1"
"c2"
;;
Fork
(
"go"
"cmp"
"c1'"
)
;;
Fork
(
"go"
"cmp"
"c2'"
)
;;
let
:
"x"
:
=
(
if
:
recv
"c1"
then
recv
"c1"
else
assert
#
false
)
in
list_
sort_elem_service_merge
"cmp"
"c"
"x"
"c1"
"c2"
.
sort_elem_service_merge
"cmp"
"c"
"x"
"c1"
"c2"
.
Definition
list_
sort_elem_service_top
:
val
:
=
λ
:
"c"
,
Definition
sort_elem_service_top
:
val
:
=
λ
:
"c"
,
let
:
"cmp"
:
=
recv
"c"
in
list_
sort_elem_service
"cmp"
"c"
.
sort_elem_service
"cmp"
"c"
.
Section
list_
sort_elem
.
Section
sort_elem
.
Context
`
{!
heapG
Σ
,
!
proto_chanG
Σ
}
(
N
:
namespace
).
Section
list_
sort_elem_inner
.
Section
sort_elem_inner
.
Context
{
A
}
(
I
:
A
→
val
→
iProp
Σ
)
(
R
:
relation
A
)
`
{!
RelDecision
R
,
!
Total
R
}.
Definition
tail_protocol_aux
(
xs
:
list
A
)
Definition
sort_elem_
tail_protocol_aux
(
xs
:
list
A
)
(
rec
:
list
A
-
d
>
iProto
Σ
)
:
list
A
-
d
>
iProto
Σ
:
=
λ
ys
,
((<?>
y
v
,
MSG
v
{{
⌜
TlRel
R
y
ys
⌝
∗
I
y
v
}}
;
(
rec
:
_
→
iProto
Σ
)
(
ys
++
[
y
]))
<&{
⌜
ys
≡
ₚ
xs
⌝
}>
END
)%
proto
.
Instance
tail_protocol_aux_contractive
xs
:
Contractive
(
tail_protocol_aux
xs
).
Instance
sort_elem_tail_protocol_aux_contractive
xs
:
Contractive
(
sort_elem_tail_protocol_aux
xs
).
Proof
.
solve_proto_contractive
.
Qed
.
Definition
tail_protocol
(
xs
:
list
A
)
:
list
A
→
iProto
Σ
:
=
fixpoint
(
tail_protocol_aux
xs
).
Global
Instance
tail_protocol_unfold
xs
ys
:
ProtoUnfold
(
tail_protocol
xs
ys
)
(
tail_protocol_aux
xs
(
tail_protocol
xs
)
ys
).
Proof
.
apply
proto_unfold_eq
,
(
fixpoint_unfold
(
tail_protocol_aux
_
)).
Qed
.
Definition
head_protocol_aux
Definition
sort_elem_tail_protocol
(
xs
:
list
A
)
:
list
A
→
iProto
Σ
:
=
fixpoint
(
sort_elem_tail_protocol_aux
xs
).
Global
Instance
sort_elem_tail_protocol_unfold
xs
ys
:
ProtoUnfold
(
sort_elem_tail_protocol
xs
ys
)
(
sort_elem_tail_protocol_aux
xs
(
sort_elem_tail_protocol
xs
)
ys
).
Proof
.
apply
proto_unfold_eq
,
(
fixpoint_unfold
(
sort_elem_tail_protocol_aux
_
)).
Qed
.
Definition
sort_elem_head_protocol_aux
(
rec
:
list
A
-
d
>
iProto
Σ
)
:
list
A
-
d
>
iProto
Σ
:
=
λ
xs
,
((<!>
x
v
,
MSG
v
{{
I
x
v
}}
;
(
rec
:
_
→
iProto
Σ
)
(
xs
++
[
x
]))
<+>
tail_protocol
xs
[])%
proto
.
<+>
sort_elem_
tail_protocol
xs
[])%
proto
.
Instance
head_protocol_aux_contractive
:
Contractive
head_protocol_aux
.
Instance
sort_elem_head_protocol_aux_contractive
:
Contractive
sort_elem_head_protocol_aux
.
Proof
.
solve_proto_contractive
.
Qed
.
Definition
head_protocol
:
list
A
→
iProto
Σ
:
=
fixpoint
head_protocol_aux
.
Global
Instance
head_protocol_unfold
xs
:
ProtoUnfold
(
head_protocol
xs
)
(
head_protocol_aux
head_protocol
xs
)
|
100
.
Proof
.
apply
proto_unfold_eq
,
(
fixpoint_unfold
head_protocol_aux
).
Qed
.
Definition
sort_elem_head_protocol
:
list
A
→
iProto
Σ
:
=
fixpoint
sort_elem_head_protocol_aux
.
Global
Instance
sort_elem_head_protocol_unfold
xs
:
ProtoUnfold
(
sort_elem_head_protocol
xs
)
(
sort_elem_head_protocol_aux
sort_elem_head_protocol
xs
).
Proof
.
apply
proto_unfold_eq
,
(
fixpoint_unfold
sort_elem_head_protocol_aux
).
Qed
.
Definition
list_
sort_elem_protocol
:
iProto
Σ
:
=
head_protocol
[].
Definition
sort_elem_protocol
:
iProto
Σ
:
=
sort_elem_
head_protocol
[].
Lemma
list_
sort_elem_service_split_spec
c
p
c1
c2
xs
xs1
xs2
:
Lemma
sort_elem_service_split_spec
c
p
c1
c2
xs
xs1
xs2
:
{{{
c
↣
iProto_dual
(
head_protocol
xs
)
<++>
p
@
N
∗
c1
↣
head_protocol
xs1
@
N
∗
c2
↣
head_protocol
xs2
@
N
c
↣
iProto_dual
(
sort_elem_
head_protocol
xs
)
<++>
p
@
N
∗
c1
↣
sort_elem_
head_protocol
xs1
@
N
∗
c2
↣
sort_elem_
head_protocol
xs2
@
N
}}}
list_
sort_elem_service_split
c
c1
c2
sort_elem_service_split
c
c1
c2
{{{
xs'
xs1'
xs2'
,
RET
#()
;
⌜
xs'
≡
ₚ
xs1'
++
xs2'
⌝
∗
c
↣
iProto_dual
(
tail_protocol
(
xs
++
xs'
)
[])
<++>
p
@
N
∗
c1
↣
tail_protocol
(
xs1
++
xs1'
)
[]
@
N
∗
c2
↣
tail_protocol
(
xs2
++
xs2'
)
[]
@
N
c
↣
iProto_dual
(
sort_elem_tail_protocol
(
xs
++
xs'
)
[])
<++>
p
@
N
∗
c1
↣
sort_elem_tail_protocol
(
xs1
++
xs1'
)
[]
@
N
∗
c2
↣
sort_elem_tail_protocol
(
xs2
++
xs2'
)
[]
@
N
}}}.
Proof
.
iIntros
(
Ψ
)
"(Hc & Hc1 & Hc2) HΨ"
.
iL
ö
b
as
"IH"
forall
(
c
c1
c2
xs
xs1
xs2
Ψ
).
...
...
@@ -111,16 +117,16 @@ Section list_sort_elem.
iApply
(
"HΨ"
$!
[]
[]
[]).
rewrite
!
right_id_L
.
by
iFrame
.
Qed
.
Lemma
list_
sort_elem_service_move_spec
c
p
cin
xs
ys
zs
xs'
ys'
:
Lemma
sort_elem_service_move_spec
c
p
cin
xs
ys
zs
xs'
ys'
:
xs
≡
ₚ
xs'
++
zs
→
ys
≡
ₚ
ys'
++
zs
→
Sorted
R
ys
→
(
∀
x
,
TlRel
R
x
ys'
→
TlRel
R
x
ys
)
→
{{{
c
↣
iProto_dual
(
tail_protocol
xs
ys
)
<++>
p
@
N
∗
cin
↣
tail_protocol
xs'
ys'
@
N
c
↣
iProto_dual
(
sort_elem_
tail_protocol
xs
ys
)
<++>
p
@
N
∗
cin
↣
sort_elem_
tail_protocol
xs'
ys'
@
N
}}}
list_
sort_elem_service_move
c
cin
sort_elem_service_move
c
cin
{{{
RET
#()
;
c
↣
p
@
N
∗
cin
↣
END
@
N
}}}.
Proof
.
iIntros
(
Hxs
Hys
Hsorted
Hrel
Ψ
)
"[Hc Hcin] HΨ"
.
...
...
@@ -139,7 +145,7 @@ Section list_sort_elem.
iApply
"HΨ"
.
iFrame
.
Qed
.
Lemma
list_
sort_elem_service_merge_spec
cmp
c
p
c1
c2
xs
ys
xs1
xs2
y1
w1
ys1
ys2
:
Lemma
sort_elem_service_merge_spec
cmp
c
p
c1
c2
xs
ys
xs1
xs2
y1
w1
ys1
ys2
:
xs
≡
ₚ
xs1
++
xs2
→
ys
≡
ₚ
ys1
++
ys2
→
Sorted
R
ys
→
...
...
@@ -147,11 +153,12 @@ Section list_sort_elem.
(
∀
x
,
TlRel
R
x
ys2
→
R
x
y1
→
TlRel
R
x
ys
)
→
cmp_spec
I
R
cmp
-
∗
{{{
c
↣
iProto_dual
(
tail_protocol
xs
ys
)
<++>
p
@
N
∗
c1
↣
tail_protocol
xs1
(
ys1
++
[
y1
])
@
N
∗
c2
↣
tail_protocol
xs2
ys2
@
N
∗
c
↣
iProto_dual
(
sort_elem_tail_protocol
xs
ys
)
<++>
p
@
N
∗
c1
↣
sort_elem_tail_protocol
xs1
(
ys1
++
[
y1
])
@
N
∗
c2
↣
sort_elem_tail_protocol
xs2
ys2
@
N
∗
I
y1
w1
}}}
list_
sort_elem_service_merge
cmp
c
w1
c1
c2
sort_elem_service_merge
cmp
c
w1
c1
c2
{{{
RET
#()
;
c
↣
p
@
N
}}}.
Proof
.
iIntros
(
Hxs
Hys
Hsort
Htl
Htl_le
)
"#Hcmp !>"
.
...
...
@@ -178,7 +185,7 @@ Section list_sort_elem.
*
intros
x'
.
inversion
1
;
discriminate_list
||
simplify_list_eq
.
by
constructor
.
-
wp_select
.
wp_send
with
"[$HIy1 //]"
.
wp_apply
(
list_
sort_elem_service_move_spec
with
"[$Hc $Hc1]"
).
wp_apply
(
sort_elem_service_move_spec
with
"[$Hc $Hc1]"
).
*
done
.
*
by
rewrite
Hys
Hys2
-!
assoc_L
(
comm
_
xs2
).
*
by
apply
Sorted_snoc
.
...
...
@@ -187,10 +194,10 @@ Section list_sort_elem.
*
iIntros
"[Hc Hc1]"
.
iApply
"HΨ"
.
iFrame
.
Qed
.
Lemma
list_
sort_elem_service_spec
cmp
c
p
:
Lemma
sort_elem_service_spec
cmp
c
p
:
cmp_spec
I
R
cmp
-
∗
{{{
c
↣
iProto_dual
list_
sort_elem_protocol
<++>
p
@
N
}}}
list_
sort_elem_service
cmp
c
{{{
c
↣
iProto_dual
sort_elem_protocol
<++>
p
@
N
}}}
sort_elem_service
cmp
c
{{{
RET
#()
;
c
↣
p
@
N
}}}.
Proof
.
iIntros
"#Hcmp !>"
(
Ψ
)
"Hc HΨ"
.
iL
ö
b
as
"IH"
forall
(
c
p
Ψ
).
...
...
@@ -199,12 +206,12 @@ Section list_sort_elem.
+
wp_recv
(
x2
v2
)
as
"HIx2"
.
wp_apply
(
new_chan_proto_spec
N
with
"[//]"
)
;
iIntros
(
cy1
cy2
)
"Hcy"
.
wp_apply
(
new_chan_proto_spec
N
with
"[//]"
)
;
iIntros
(
cz1
cz2
)
"Hcz"
.
iMod
(
"Hcy"
$!
(
list_
sort_elem_protocol
<++>
END
)%
proto
)
as
"[Hcy1 Hcy2]"
.
iMod
(
"Hcz"
$!
(
list_
sort_elem_protocol
<++>
END
)%
proto
)
as
"[Hcz1 Hcz2]"
.
iMod
(
"Hcy"
$!
(
sort_elem_protocol
<++>
END
)%
proto
)
as
"[Hcy1 Hcy2]"
.
iMod
(
"Hcz"
$!
(
sort_elem_protocol
<++>
END
)%
proto
)
as
"[Hcz1 Hcz2]"
.
iEval
(
rewrite
right_id
)
in
"Hcy1 Hcz1"
.
wp_select
.
wp_send
with
"[$HIx1]"
.
wp_select
.
wp_send
with
"[$HIx2]"
.
wp_apply
(
list_
sort_elem_service_split_spec
with
"[$Hc $Hcy1 $Hcz1]"
).
wp_apply
(
sort_elem_service_split_spec
with
"[$Hc $Hcy1 $Hcz1]"
).
iIntros
(
xs'
xs1'
xs2'
)
;
iDestruct
1
as
(
Hxs'
)
"(Hc & Hcy & Hcz) /="
.
wp_apply
(
wp_fork
with
"[Hcy2]"
).
{
iNext
.
wp_apply
(
"IH"
with
"Hcy2"
)
;
auto
.
}
...
...
@@ -212,28 +219,28 @@ Section list_sort_elem.
{
iNext
.
wp_apply
(
"IH"
with
"Hcz2"
)
;
auto
.
}
wp_branch
as
%
_
|
%[]%
Permutation_nil_cons
.
wp_recv
(
x
v
)
as
"[_ HIx]"
.
wp_apply
(
list_
sort_elem_service_merge_spec
_
_
_
_
_
_
[]
_
_
_
_
[]
[]
wp_apply
(
sort_elem_service_merge_spec
_
_
_
_
_
_
[]
_
_
_
_
[]
[]
with
"Hcmp [$Hc $Hcy $Hcz $HIx]"
)
;
simpl
;
auto
using
TlRel_nil
,
Sorted_nil
.
by
rewrite
Hxs'
Permutation_middle
.
+
wp_select
.
wp_send
with
"[$HIx1]"
;
first
by
auto
using
TlRel_nil
.
wp_select
.
by
iApply
"HΨ"
.
-
wp_select
.
by
iApply
"HΨ"
.
Qed
.
End
list_
sort_elem_inner
.
End
sort_elem_inner
.
Definition
list_
sort_elem_top_protocol
:
iProto
Σ
:
=
Definition
sort_elem_top_protocol
:
iProto
Σ
:
=
(<!>
A
(
I
:
A
→
val
→
iProp
Σ
)
(
R
:
A
→
A
→
Prop
)
`
{!
RelDecision
R
,
!
Total
R
}
(
cmp
:
val
),
MSG
cmp
{{
cmp_spec
I
R
cmp
}}
;
head_protocol
I
R
[])%
proto
.
sort_elem_
head_protocol
I
R
[])%
proto
.
Lemma
list_
sort_elem_service_top_spec
c
p
:
{{{
c
↣
iProto_dual
list_
sort_elem_top_protocol
<++>
p
@
N
}}}
list_
sort_elem_service_top
c
Lemma
sort_elem_service_top_spec
c
p
:
{{{
c
↣
iProto_dual
sort_elem_top_protocol
<++>
p
@
N
}}}
sort_elem_service_top
c
{{{
RET
#()
;
c
↣
p
@
N
}}}.
Proof
.
iIntros
(
Ψ
)
"Hc HΨ"
.
wp_lam
.
wp_recv
(
?
I
R
?
?
cmp
)
as
"#Hcmp"
.
by
wp_apply
(
list_
sort_elem_service_spec
with
"Hcmp Hc"
).
wp_recv
(
A
I
R
?
?
cmp
)
as
"#Hcmp"
.
by
wp_apply
(
sort_elem_service_spec
with
"Hcmp Hc"
).
Qed
.
End
list_
sort_elem
.
End
sort_elem
.
theories/examples/
list_
sort_elem_client.v
→
theories/examples/sort_elem_client.v
View file @
1fa2c070
...
...
@@ -3,7 +3,7 @@ From osiris.channel Require Import proto_channel proofmode.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
From
iris
.
heap_lang
Require
Import
assert
.
From
osiris
.
utils
Require
Import
list
compare
.
From
osiris
.
examples
Require
Import
list_
sort_elem
.
From
osiris
.
examples
Require
Import
sort_elem
.
Definition
send_all
:
val
:
=
rec
:
"go"
"c"
"xs"
:
=
...
...
@@ -18,21 +18,21 @@ Definition recv_all : val :=
then
let
:
"x"
:
=
recv
"c"
in
lcons
"x"
(
"go"
"c"
)
else
lnil
#().
Definition
list_
sort_elem_client
:
val
:
=
Definition
sort_elem_client
:
val
:
=
λ
:
"cmp"
"xs"
,
let
:
"c"
:
=
start_chan
list_
sort_elem_service_top
in
let
:
"c"
:
=
start_chan
sort_elem_service_top
in
send
"c"
"cmp"
;;
send_all
"c"
"xs"
;;
recv_all
"c"
.
Section
list_
sort_elem_client
.
Section
sort_elem_client
.
Context
`
{!
heapG
Σ
,
!
proto_chanG
Σ
}
(
N
:
namespace
).
Context
{
A
}
(
I
:
A
→
val
→
iProp
Σ
)
(
R
:
relation
A
)
`
{!
RelDecision
R
,
!
Total
R
}.
Lemma
send_all_spec
c
p
xs'
xs
vs
:
{{{
c
↣
head_protocol
I
R
xs'
<++>
p
@
N
∗
[
∗
list
]
x
;
v
∈
xs
;
vs
,
I
x
v
}}}
{{{