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
12dc9a35
Commit
12dc9a35
authored
Mar 25, 2020
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Consistently use `Recv`.
parent
31806a14
Pipeline
#25635
failed with stage
in 9 seconds
Changes
4
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
42 additions
and
42 deletions
+42
-42
theories/channel/channel.v
theories/channel/channel.v
+9
-9
theories/channel/proofmode.v
theories/channel/proofmode.v
+3
-3
theories/channel/proto.v
theories/channel/proto.v
+27
-27
theories/channel/proto_model.v
theories/channel/proto_model.v
+3
-3
No files found.
theories/channel/channel.v
View file @
12dc9a35
...
...
@@ -3,7 +3,7 @@ lock-protected buffers, and their primitive proof rules. Moreover:
- It defines the connective [c ↣ prot] for ownership of channel endpoints,
which describes that channel endpoint [c] adheres to protocol [prot].
- It proves Actris's specifications of [send] and [rec
eive
] w.r.t. dependent
- It proves Actris's specifications of [send] and [rec
v
] w.r.t. dependent
separation protocols.
An encoding of the usual branching connectives [prot1 <{Q1}+{Q2}> prot2] and
...
...
@@ -104,13 +104,13 @@ Typeclasses Opaque iProto_branch.
Arguments
iProto_branch
{
_
}
_
_
%
I
_
%
I
_
%
proto
_
%
proto
.
Instance
:
Params
(@
iProto_branch
)
2
:
=
{}.
Infix
"<{ P1 }+{ P2 }>"
:
=
(
iProto_branch
Send
P1
P2
)
(
at
level
85
)
:
proto_scope
.
Infix
"<{ P1 }&{ P2 }>"
:
=
(
iProto_branch
Rec
eive
P1
P2
)
(
at
level
85
)
:
proto_scope
.
Infix
"<{ P1 }&{ P2 }>"
:
=
(
iProto_branch
Rec
v
P1
P2
)
(
at
level
85
)
:
proto_scope
.
Infix
"<+{ P2 }>"
:
=
(
iProto_branch
Send
True
P2
)
(
at
level
85
)
:
proto_scope
.
Infix
"<&{ P2 }>"
:
=
(
iProto_branch
Rec
eive
True
P2
)
(
at
level
85
)
:
proto_scope
.
Infix
"<&{ P2 }>"
:
=
(
iProto_branch
Rec
v
True
P2
)
(
at
level
85
)
:
proto_scope
.
Infix
"<{ P1 }+>"
:
=
(
iProto_branch
Send
P1
True
)
(
at
level
85
)
:
proto_scope
.
Infix
"<{ P1 }&>"
:
=
(
iProto_branch
Rec
eive
P1
True
)
(
at
level
85
)
:
proto_scope
.
Infix
"<{ P1 }&>"
:
=
(
iProto_branch
Rec
v
P1
True
)
(
at
level
85
)
:
proto_scope
.
Infix
"<+>"
:
=
(
iProto_branch
Send
True
True
)
(
at
level
85
)
:
proto_scope
.
Infix
"<&>"
:
=
(
iProto_branch
Rec
eive
True
True
)
(
at
level
85
)
:
proto_scope
.
Infix
"<&>"
:
=
(
iProto_branch
Rec
v
True
True
)
(
at
level
85
)
:
proto_scope
.
Section
channel
.
Context
`
{!
heapG
Σ
,
!
chanG
Σ
}.
...
...
@@ -233,9 +233,9 @@ Section channel.
Qed
.
Lemma
try_recv_spec_packed
{
TT
}
c
(
pc
:
TT
→
val
*
iProp
Σ
*
iProto
Σ
)
:
{{{
c
↣
iProto_message
Rec
eive
pc
}}}
{{{
c
↣
iProto_message
Rec
v
pc
}}}
try_recv
c
{{{
v
,
RET
v
;
(
⌜
v
=
NONEV
⌝
∧
c
↣
iProto_message
Rec
eive
pc
)
∨
{{{
v
,
RET
v
;
(
⌜
v
=
NONEV
⌝
∧
c
↣
iProto_message
Rec
v
pc
)
∨
(
∃
x
:
TT
,
⌜
v
=
SOMEV
((
pc
x
).
1
.
1
)
⌝
∗
c
↣
(
pc
x
).
2
∗
(
pc
x
).
1
.
2
)
}}}.
Proof
.
rewrite
iProto_mapsto_eq
.
iIntros
(
Φ
)
"Hc HΦ"
.
wp_lam
;
wp_pures
.
...
...
@@ -267,7 +267,7 @@ Section channel.
Qed
.
Lemma
recv_spec_packed
{
TT
}
c
(
pc
:
TT
→
val
*
iProp
Σ
*
iProto
Σ
)
:
{{{
c
↣
iProto_message
Rec
eive
pc
}}}
{{{
c
↣
iProto_message
Rec
v
pc
}}}
recv
c
{{{
x
,
RET
(
pc
x
).
1
.
1
;
c
↣
(
pc
x
).
2
∗
(
pc
x
).
1
.
2
}}}.
Proof
.
...
...
@@ -280,7 +280,7 @@ Section channel.
(** A version written without Texan triples that is more convenient to use
(via [iApply] in Coq. *)
Lemma
recv_spec
{
TT
}
Φ
c
(
pc
:
TT
→
val
*
iProp
Σ
*
iProto
Σ
)
:
c
↣
iProto_message
Rec
eive
pc
-
∗
c
↣
iProto_message
Rec
v
pc
-
∗
▷
(
∀
..
x
:
TT
,
c
↣
(
pc
x
).
2
-
∗
(
pc
x
).
1
.
2
-
∗
Φ
(
pc
x
).
1
.
1
)
-
∗
WP
recv
c
{{
Φ
}}.
Proof
.
...
...
theories/channel/proofmode.v
View file @
12dc9a35
...
...
@@ -33,8 +33,8 @@ Class ActionDualIf (d : bool) (a1 a2 : action) :=
Hint
Mode
ActionDualIf
!
!
-
:
typeclass_instances
.
Instance
action_dual_if_false
a
:
ActionDualIf
false
a
a
:
=
eq_refl
.
Instance
action_dual_if_true_send
:
ActionDualIf
true
Send
Rec
eive
:
=
eq_refl
.
Instance
action_dual_if_true_rec
eive
:
ActionDualIf
true
Rec
eive
Send
:
=
eq_refl
.
Instance
action_dual_if_true_send
:
ActionDualIf
true
Send
Rec
v
:
=
eq_refl
.
Instance
action_dual_if_true_rec
v
:
ActionDualIf
true
Rec
v
Send
:
=
eq_refl
.
Class
ProtoNormalize
{
Σ
}
(
d
:
bool
)
(
p
:
iProto
Σ
)
(
pas
:
list
(
bool
*
iProto
Σ
))
(
q
:
iProto
Σ
)
:
=
...
...
@@ -166,7 +166,7 @@ End classes.
Lemma
tac_wp_recv
`
{!
chanG
Σ
,
!
heapG
Σ
}
{
TT
:
tele
}
Δ
i
j
K
c
p
(
pc
:
TT
→
val
*
iProp
Σ
*
iProto
Σ
)
Φ
:
envs_lookup
i
Δ
=
Some
(
false
,
c
↣
p
)%
I
→
ProtoNormalize
false
p
[]
(
iProto_message
Rec
eive
pc
)
→
ProtoNormalize
false
p
[]
(
iProto_message
Rec
v
pc
)
→
let
Δ
'
:
=
envs_delete
false
i
false
Δ
in
(
∀
..
x
:
TT
,
match
envs_app
false
...
...
theories/channel/proto.v
View file @
12dc9a35
...
...
@@ -121,24 +121,24 @@ Notation "<!> 'MSG' v ; p" :=
Notation
"<?> x1 .. xn , 'MSG' v {{ P } } ; p"
:
=
(
iProto_message
Rec
eive
Rec
v
(
tele_app
(
TT
:
=
TeleS
(
λ
x1
,
..
(
TeleS
(
λ
xn
,
TeleO
))
..
))
$
λ
x1
,
..
(
λ
xn
,
(
v
%
V
,
P
%
I
,
p
%
proto
))
..))
(
at
level
20
,
x1
binder
,
xn
binder
,
v
at
level
20
,
P
,
p
at
level
200
)
:
proto_scope
.
Notation
"<?> x1 .. xn , 'MSG' v ; p"
:
=
(
iProto_message
Rec
eive
Rec
v
(
tele_app
(
TT
:
=
TeleS
(
λ
x1
,
..
(
TeleS
(
λ
xn
,
TeleO
))
..
))
$
λ
x1
,
..
(
λ
xn
,
(
v
%
V
,
True
%
I
,
p
%
proto
))
..))
(
at
level
20
,
x1
binder
,
xn
binder
,
v
at
level
20
,
p
at
level
200
)
:
proto_scope
.
Notation
"<?> 'MSG' v {{ P } } ; p"
:
=
(
iProto_message
Rec
eive
Rec
v
(
tele_app
(
TT
:
=
TeleO
)
(
v
%
V
,
P
%
I
,
p
%
proto
)))
(
at
level
20
,
v
at
level
20
,
P
,
p
at
level
200
)
:
proto_scope
.
Notation
"<?> 'MSG' v ; p"
:
=
(
iProto_message
Rec
eive
Rec
v
(
tele_app
(
TT
:
=
TeleO
)
(
v
%
V
,
True
%
I
,
p
%
proto
)))
(
at
level
20
,
v
at
level
20
,
p
at
level
200
)
:
proto_scope
.
...
...
@@ -190,21 +190,21 @@ Definition iProto_le_pre {Σ V}
p1
≡
proto_message
a1
pc1
∗
p2
≡
proto_message
a2
pc2
∗
match
a1
,
a2
with
|
Rec
eive
,
Rec
eive
=>
|
Rec
v
,
Rec
v
=>
∀
v
p1'
,
pc1
v
(
proto_eq_next
p1'
)
-
∗
◇
∃
p2'
,
▷
rec
p1'
p2'
∗
pc2
v
(
proto_eq_next
p2'
)
|
Send
,
Send
=>
∀
v
p2'
,
pc2
v
(
proto_eq_next
p2'
)
-
∗
◇
∃
p1'
,
▷
rec
p1'
p2'
∗
pc1
v
(
proto_eq_next
p1'
)
|
Rec
eive
,
Send
=>
|
Rec
v
,
Send
=>
∀
v1
v2
p1'
p2'
,
pc1
v1
(
proto_eq_next
p1'
)
-
∗
pc2
v2
(
proto_eq_next
p2'
)
-
∗
◇
∃
pc1'
pc2'
pt
,
▷
rec
p1'
(
proto_message
Send
pc1'
)
∗
▷
rec
(
proto_message
Rec
eive
pc2'
)
p2'
∗
▷
rec
(
proto_message
Rec
v
pc2'
)
p2'
∗
pc1'
v2
(
proto_eq_next
pt
)
∗
pc2'
v1
(
proto_eq_next
pt
)
|
Send
,
Rec
eive
=>
False
|
Send
,
Rec
v
=>
False
end
.
Instance
iProto_le_pre_ne
{
Σ
V
}
(
rec
:
iProto
Σ
V
→
iProto
Σ
V
→
iProp
Σ
)
:
NonExpansive2
(
iProto_le_pre
rec
).
...
...
@@ -235,12 +235,12 @@ Fixpoint iProto_interp_aux {Σ V} (n : nat)
|
S
n
=>
(
∃
vl
vsl'
pc
p2'
,
⌜
vsl
=
vl
::
vsl'
⌝
∗
iProto_le
(
proto_message
Rec
eive
pc
)
pr
∗
iProto_le
(
proto_message
Rec
v
pc
)
pr
∗
pc
vl
(
proto_eq_next
p2'
)
∗
iProto_interp_aux
n
vsl'
vsr
pl
p2'
)
∨
(
∃
vr
vsr'
pc
p1'
,
⌜
vsr
=
vr
::
vsr'
⌝
∗
iProto_le
(
proto_message
Rec
eive
pc
)
pl
∗
iProto_le
(
proto_message
Rec
v
pc
)
pl
∗
pc
vr
(
proto_eq_next
p1'
)
∗
iProto_interp_aux
n
vsl
vsr'
p1'
pr
)
end
.
...
...
@@ -431,12 +431,12 @@ Section proto.
|
Send
=>
∀
v
p2'
,
pc2
v
(
proto_eq_next
p2'
)
-
∗
◇
∃
p1'
,
▷
iProto_le
p1'
p2'
∗
pc1
v
(
proto_eq_next
p1'
)
|
Rec
eive
=>
|
Rec
v
=>
∀
v1
v2
p1'
p2'
,
pc1
v1
(
proto_eq_next
p1'
)
-
∗
pc2
v2
(
proto_eq_next
p2'
)
-
∗
◇
∃
pc1'
pc2'
pt
,
▷
iProto_le
p1'
(
proto_message
Send
pc1'
)
∗
▷
iProto_le
(
proto_message
Rec
eive
pc2'
)
p2'
∗
▷
iProto_le
(
proto_message
Rec
v
pc2'
)
p2'
∗
pc1'
v2
(
proto_eq_next
pt
)
∗
pc2'
v1
(
proto_eq_next
pt
)
end
.
...
...
@@ -451,8 +451,8 @@ Section proto.
Qed
.
Lemma
iProto_le_recv_inv
p1
pc2
:
iProto_le
p1
(
proto_message
Rec
eive
pc2
)
-
∗
∃
pc1
,
p1
≡
proto_message
Rec
eive
pc1
∗
iProto_le
p1
(
proto_message
Rec
v
pc2
)
-
∗
∃
pc1
,
p1
≡
proto_message
Rec
v
pc1
∗
∀
v
p1'
,
pc1
v
(
proto_eq_next
p1'
)
-
∗
◇
∃
p2'
,
▷
iProto_le
p1'
p2'
∗
pc2
v
(
proto_eq_next
p2'
).
Proof
.
...
...
@@ -542,7 +542,7 @@ Section proto.
⌜
(
pc1
x1
).
1
.
1
=
(
pc2
x2
).
1
.
1
⌝
∗
▷
(
pc2
x2
).
1
.
2
∗
▷
iProto_le
(
pc1
x1
).
2
(
pc2
x2
).
2
)
-
∗
iProto_le
(
iProto_message
Rec
eive
pc1
)
(
iProto_message
Rec
eive
pc2
).
iProto_le
(
iProto_message
Rec
v
pc1
)
(
iProto_message
Rec
v
pc2
).
Proof
.
iIntros
"H"
.
rewrite
iProto_le_unfold
iProto_message_eq
.
iRight
.
iExists
_
,
_
,
_
,
_;
do
2
(
iSplit
;
[
done
|]).
...
...
@@ -557,7 +557,7 @@ Section proto.
⌜
(
pc1
x1
).
1
.
1
=
(
pc2
x2
).
1
.
1
⌝
∗
(
pc2
x2
).
1
.
2
∗
iProto_le
(
pc1
x1
).
2
(
pc2
x2
).
2
)
-
∗
iProto_le
(
iProto_message
Rec
eive
pc1
)
(
iProto_message
Rec
eive
pc2
).
iProto_le
(
iProto_message
Rec
v
pc1
)
(
iProto_message
Rec
v
pc2
).
Proof
.
iIntros
"H"
.
iApply
iProto_le_recv
.
iIntros
(
x2
)
"Hpc"
.
rewrite
bi_tforall_forall
.
iDestruct
(
"H"
with
"Hpc"
)
as
"H"
.
...
...
@@ -574,10 +574,10 @@ Section proto.
⌜
(
pc1
x1
).
1
.
1
=
(
pc4
x4
).
1
.
1
⌝
∗
⌜
(
pc2
x2
).
1
.
1
=
(
pc3
x3
).
1
.
1
⌝
∗
▷
iProto_le
(
pc1
x1
).
2
(
iProto_message
Send
pc3
)
∗
▷
iProto_le
(
iProto_message
Rec
eive
pc4
)
(
pc2
x2
).
2
∗
▷
iProto_le
(
iProto_message
Rec
v
pc4
)
(
pc2
x2
).
2
∗
▷
(
pc3
x3
).
1
.
2
∗
▷
(
pc4
x4
).
1
.
2
∗
▷
((
pc3
x3
).
2
≡
(
pc4
x4
).
2
))
-
∗
iProto_le
(
iProto_message
Rec
eive
pc1
)
(
iProto_message
Send
pc2
).
iProto_le
(
iProto_message
Rec
v
pc1
)
(
iProto_message
Send
pc2
).
Proof
.
iIntros
"H"
.
rewrite
iProto_le_unfold
iProto_message_eq
.
iRight
.
iExists
_
,
_
,
_
,
_;
do
2
(
iSplit
;
[
done
|])
;
simpl
.
...
...
@@ -598,10 +598,10 @@ Section proto.
⌜
(
pc1
x1
).
1
.
1
=
(
pc4
x4
).
1
.
1
⌝
∗
⌜
(
pc2
x2
).
1
.
1
=
(
pc3
x3
).
1
.
1
⌝
∗
iProto_le
(
pc1
x1
).
2
(
iProto_message
Send
pc3
)
∗
iProto_le
(
iProto_message
Rec
eive
pc4
)
(
pc2
x2
).
2
∗
iProto_le
(
iProto_message
Rec
v
pc4
)
(
pc2
x2
).
2
∗
(
pc3
x3
).
1
.
2
∗
(
pc4
x4
).
1
.
2
∗
((
pc3
x3
).
2
≡
(
pc4
x4
).
2
))
-
∗
iProto_le
(
iProto_message
Rec
eive
pc1
)
(
iProto_message
Send
pc2
).
iProto_le
(
iProto_message
Rec
v
pc1
)
(
iProto_message
Send
pc2
).
Proof
.
iIntros
"H"
.
iApply
iProto_le_swap
.
iIntros
(
x1
x2
)
"Hpc1 Hpc2"
.
repeat
setoid_rewrite
bi_tforall_forall
.
iDestruct
(
"H"
with
"Hpc1 Hpc2"
)
as
"H"
.
...
...
@@ -618,10 +618,10 @@ Section proto.
Lemma
iProto_le_swap_simple
{
TT1
TT2
}
(
v1
:
TT1
→
V
)
(
v2
:
TT2
→
V
)
(
P1
:
TT1
→
iProp
Σ
)
(
P2
:
TT2
→
iProp
Σ
)
(
p
:
TT1
→
TT2
→
iProto
Σ
V
)
:
⊢
iProto_le
(
iProto_message
Rec
eive
(
λ
x1
,
(
iProto_message
Rec
v
(
λ
x1
,
(
v1
x1
,
P1
x1
,
iProto_message
Send
(
λ
x2
,
(
v2
x2
,
P2
x2
,
p
x1
x2
)))))
(
iProto_message
Send
(
λ
x2
,
(
v2
x2
,
P2
x2
,
iProto_message
Rec
eive
(
λ
x1
,
(
v1
x1
,
P1
x1
,
p
x1
x2
))))).
(
v2
x2
,
P2
x2
,
iProto_message
Rec
v
(
λ
x1
,
(
v1
x1
,
P1
x1
,
p
x1
x2
))))).
Proof
.
iApply
iProto_le_swap
.
iIntros
(
x1
x2
)
"/= HP1 HP2"
.
iExists
TT2
,
TT1
,
(
λ
x2
,
(
v2
x2
,
P2
x2
,
p
x1
x2
)),
...
...
@@ -717,12 +717,12 @@ Section proto.
iProto_le
(
iProto_dual
p
)
pr
)
∨
(
∃
vl
vsl'
pc
pr'
,
⌜
vsl
=
vl
::
vsl'
⌝
∗
iProto_le
(
proto_message
Rec
eive
pc
)
pr
∗
iProto_le
(
proto_message
Rec
v
pc
)
pr
∗
pc
vl
(
proto_eq_next
pr'
)
∗
iProto_interp
vsl'
vsr
pl
pr'
)
∨
(
∃
vr
vsr'
pc
pl'
,
⌜
vsr
=
vr
::
vsr'
⌝
∗
iProto_le
(
proto_message
Rec
eive
pc
)
pl
∗
iProto_le
(
proto_message
Rec
v
pc
)
pl
∗
pc
vr
(
proto_eq_next
pl'
)
∗
iProto_interp
vsl
vsr'
pl'
pr
).
Proof
.
...
...
@@ -824,7 +824,7 @@ Section proto.
Lemma
iProto_interp_recv
vl
vsl
vsr
pl
pr
pcr
:
iProto_interp
(
vl
::
vsl
)
vsr
pl
pr
-
∗
iProto_le
pr
(
proto_message
Rec
eive
pcr
)
-
∗
iProto_le
pr
(
proto_message
Rec
v
pcr
)
-
∗
◇
∃
pr
,
pcr
vl
(
proto_eq_next
pr
)
∗
▷
iProto_interp
vsl
vsr
pl
pr
.
Proof
.
iIntros
"H Hle"
.
iDestruct
(
iProto_interp_le_r
with
"H Hle"
)
as
"H"
.
...
...
@@ -916,7 +916,7 @@ Section proto.
Lemma
iProto_recv_l
{
TT
}
γ
(
pc
:
TT
→
V
*
iProp
Σ
*
iProto
Σ
V
)
vr
vsr
vsl
:
iProto_ctx
γ
vsl
(
vr
::
vsr
)
-
∗
iProto_own
γ
Left
(
iProto_message
Rec
eive
pc
)
==
∗
iProto_own
γ
Left
(
iProto_message
Rec
v
pc
)
==
∗
▷
▷
∃
(
x
:
TT
),
⌜
vr
=
(
pc
x
).
1
.
1
⌝
∗
iProto_ctx
γ
vsl
vsr
∗
...
...
@@ -938,7 +938,7 @@ Section proto.
Lemma
iProto_recv_r
{
TT
}
γ
(
pc
:
TT
→
V
*
iProp
Σ
*
iProto
Σ
V
)
vl
vsr
vsl
:
iProto_ctx
γ
(
vl
::
vsl
)
vsr
-
∗
iProto_own
γ
Right
(
iProto_message
Rec
eive
pc
)
==
∗
iProto_own
γ
Right
(
iProto_message
Rec
v
pc
)
==
∗
▷
▷
∃
(
x
:
TT
),
⌜
vl
=
(
pc
x
).
1
.
1
⌝
∗
iProto_ctx
γ
vsl
vsr
∗
...
...
theories/channel/proto_model.v
View file @
12dc9a35
...
...
@@ -13,7 +13,7 @@ recursive domain equation:
Here, the left-hand side of the sum is used for the terminated process, while
the right-hand side is used for the communication constructors. The type
[action] is an inductively defined datatype with two constructors [Send] and
[Rec
eive
]. Compared to having an additional sum in [proto], this makes it
[Rec
v
]. Compared to having an additional sum in [proto], this makes it
possible to factorize the code in a better way.
The remainder [V → (▶ proto → PROP) → PROP)] is a predicate that ranges over
...
...
@@ -39,10 +39,10 @@ From iris.algebra Require Import cofe_solver.
Set
Default
Proof
Using
"Type"
.
Module
Export
action
.
Inductive
action
:
=
Send
|
Rec
eive
.
Inductive
action
:
=
Send
|
Rec
v
.
Instance
action_inhabited
:
Inhabited
action
:
=
populate
Send
.
Definition
action_dual
(
a
:
action
)
:
action
:
=
match
a
with
Send
=>
Rec
eive
|
Rec
eive
=>
Send
end
.
match
a
with
Send
=>
Rec
v
|
Rec
v
=>
Send
end
.
Instance
action_dual_involutive
:
Involutive
(=)
action_dual
.
Proof
.
by
intros
[].
Qed
.
Canonical
Structure
actionO
:
=
leibnizO
action
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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