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
0bc616f0
Commit
0bc616f0
authored
Apr 24, 2020
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Refactor.
Kinded subtyping, better file structure, more setoid stuff, reorganize imports.
parent
4e372fb3
Pipeline
#27119
failed with stage
in 9 minutes and 47 seconds
Changes
17
Pipelines
1
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
17 changed files
with
1121 additions
and
1246 deletions
+1121
-1246
_CoqProject
_CoqProject
+7
-4
opam
opam
+2
-2
theories/channel/channel.v
theories/channel/channel.v
+2
-1
theories/channel/proto.v
theories/channel/proto.v
+2
-1
theories/logrel/copying.v
theories/logrel/copying.v
+0
-221
theories/logrel/environments.v
theories/logrel/environments.v
+162
-0
theories/logrel/examples/double.v
theories/logrel/examples/double.v
+7
-13
theories/logrel/examples/pair.v
theories/logrel/examples/pair.v
+2
-4
theories/logrel/lsty.v
theories/logrel/lsty.v
+0
-46
theories/logrel/model.v
theories/logrel/model.v
+58
-119
theories/logrel/operators.v
theories/logrel/operators.v
+71
-0
theories/logrel/session_types.v
theories/logrel/session_types.v
+41
-92
theories/logrel/subtyping.v
theories/logrel/subtyping.v
+34
-495
theories/logrel/subtyping_rules.v
theories/logrel/subtyping_rules.v
+433
-0
theories/logrel/term_types.v
theories/logrel/term_types.v
+163
-0
theories/logrel/term_typing_rules.v
theories/logrel/term_typing_rules.v
+96
-248
theories/logrel/typing_judgment.v
theories/logrel/typing_judgment.v
+41
-0
No files found.
_CoqProject
View file @
0bc616f0
...
...
@@ -18,10 +18,13 @@ theories/examples/sort_fg.v
theories/examples/map.v
theories/examples/map_reduce.v
theories/logrel/model.v
theories/logrel/ltyping.v
theories/logrel/session_types.v
theories/logrel/types.v
theories/logrel/subtyping.v
theories/logrel/copying.v
theories/logrel/environments.v
theories/logrel/term_types.v
theories/logrel/session_types.v
theories/logrel/operators.v
theories/logrel/typing_judgment.v
theories/logrel/subtyping_rules.v
theories/logrel/term_typing_rules.v
theories/logrel/examples/double.v
theories/logrel/examples/pair.v
opam
View file @
0bc616f0
opam-version: "1.2"
name: "coq-actris"
maintainer: "Robbert Krebbers"
authors: "Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers"
authors: "Jonas Kastberg Hinrichsen,
Daniël Louwrink,
Jesper Bengtson, Robbert Krebbers"
license: "BSD"
bug-reports: "https://gitlab.mpi-sws.org/iris/actris/issues"
dev-repo: "https://gitlab.mpi-sws.org/iris/actris.git"
...
...
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
depends: [
"coq-iris" { (= "dev.2020-04-
13
.0.
26dc475b
") | (= "dev") }
"coq-iris" { (= "dev.2020-04-
24
.0.
9cc3cc77
") | (= "dev") }
]
theories/channel/channel.v
View file @
0bc616f0
...
...
@@ -18,7 +18,8 @@ In this file we define the three message-passing connectives:
- [send] takes an endpoint and adds an element to the first buffer.
- [recv] performs a busy loop until there is something in the second buffer,
which it pops and returns, locking during each peek.*)
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
From
iris
.
heap_lang
Require
Export
lifting
notation
.
From
iris
.
heap_lang
Require
Import
proofmode
.
From
iris
.
heap_lang
.
lib
Require
Import
spin_lock
.
From
actris
.
channel
Require
Export
proto
.
From
actris
.
utils
Require
Import
llist
skip
.
...
...
theories/channel/proto.v
View file @
0bc616f0
...
...
@@ -25,9 +25,10 @@ specifications of the message-passing primitives are defined in terms of the
protocol connectives. *)
From
iris
.
algebra
Require
Import
excl_auth
.
From
iris
.
bi
Require
Import
telescopes
.
From
iris
.
program_logic
Require
Import
language
.
From
iris
.
proofmode
Require
Import
tactics
.
From
iris
.
base_logic
Require
Export
lib
.
iprop
.
From
iris
.
base_logic
Require
Import
lib
.
own
.
From
iris
.
program_logic
Require
Import
language
.
From
actris
.
channel
Require
Import
proto_model
.
Set
Default
Proof
Using
"Type"
.
Export
action
.
...
...
theories/logrel/copying.v
deleted
100644 → 0
View file @
4e372fb3
From
actris
.
logrel
Require
Import
ltyping
types
subtyping
.
From
actris
.
channel
Require
Import
channel
.
From
iris
.
base_logic
.
lib
Require
Import
invariants
.
From
iris
.
proofmode
Require
Import
tactics
.
From
iris
.
heap_lang
Require
Import
notation
proofmode
.
From
iris
.
bi
.
lib
Require
Export
core
.
(* TODO: Coq fails to infer what the Σ should be if I move some of these
definitions out of the section or into a different section with its own Context
declaration. *)
Section
copying
.
Context
`
{
heapG
Σ
,
chanG
Σ
}.
Implicit
Types
A
:
lty
Σ
.
Implicit
Types
S
:
lsty
Σ
.
(* We define the copyability of semantic types in terms of subtyping. *)
Definition
copyable
(
A
:
lty
Σ
)
:
iProp
Σ
:
=
A
<
:
copy
A
.
(* Subtyping for `copy` and `copy-` *)
Lemma
lty_le_copy
A
:
⊢
copy
A
<
:
A
.
Proof
.
by
iIntros
(
v
)
"!> #H"
.
Qed
.
(* TODO(COPY): Show derived rules about copyability of products, sums, etc. *)
(* TODO(COPY): Commuting rule for μ, allowing `copy` to move outside the μ *)
Lemma
lty_le_copy_minus_copy
A
:
⊢
copy
-
(
copy
A
)
<
:
A
.
Proof
.
iIntros
(
v
)
"!> #Hv"
.
iDestruct
(
coreP_elim
with
"Hv"
)
as
"Hw"
.
iApply
"Hw"
.
Qed
.
Lemma
lty_le_copy_minus
A
:
⊢
A
<
:
copy
-
A
.
Proof
.
iIntros
"!>"
(
v
).
iApply
coreP_intro
.
Qed
.
(* TODO: Wait for this to be merged into Iris and then bump Iris version *)
Lemma
actris_coreP_wand
(
P
Q
:
iProp
Σ
)
:
<
affine
>
■
(
P
-
∗
Q
)
-
∗
coreP
P
-
∗
coreP
Q
.
Proof
.
rewrite
/
coreP
.
iIntros
"#HPQ HP"
(
R
)
"#HR #HQR"
.
iApply
(
"HP"
with
"HR"
).
iIntros
"!> !> HP"
.
iApply
"HQR"
.
by
iApply
"HPQ"
.
Qed
.
Lemma
lty_copy_minus_mono
A
B
:
A
<
:
B
-
∗
copy
-
A
<
:
copy
-
B
.
Proof
.
iIntros
"#Hsub !>"
(
v
)
"#HA"
.
iApply
(
actris_coreP_wand
(
A
v
)).
-
iModIntro
.
iClear
"HA"
.
iModIntro
.
iApply
"Hsub"
.
-
iApply
"HA"
.
Qed
.
(* Copyability of types *)
Lemma
lty_unit_copyable
:
⊢
copyable
().
Proof
.
iIntros
(
v
)
"!> #Hv !>"
.
iFrame
"Hv"
.
Qed
.
Lemma
lty_bool_copyable
:
⊢
copyable
lty_bool
.
Proof
.
iIntros
(
v
)
"!> #Hv !>"
.
iFrame
"Hv"
.
Qed
.
Lemma
lty_int_copyable
:
⊢
copyable
lty_int
.
Proof
.
iIntros
(
v
)
"!> #Hv !>"
.
iFrame
"Hv"
.
Qed
.
(* TODO: Use Iris quantification here instead of Coq quantification? (Or doesn't matter?) *)
Lemma
lty_copy_copyable
A
:
⊢
copyable
(
copy
A
).
Proof
.
iIntros
(
v
)
"!> #Hv !>"
.
iFrame
"Hv"
.
Qed
.
Lemma
lty_copyminus_copyable
A
:
⊢
copyable
(
copy
-
A
).
Proof
.
iIntros
(
v
)
"!> #Hv !>"
.
iFrame
"Hv"
.
Qed
.
Lemma
lty_any_copyable
:
⊢
copyable
any
.
Proof
.
iIntros
(
v
)
"!> #Hv !>"
.
iFrame
"Hv"
.
Qed
.
Lemma
lty_ref_shr_copyable
A
:
⊢
copyable
(
ref_shr
A
).
Proof
.
iIntros
(
v
)
"!> #Hv !>"
.
iFrame
"Hv"
.
Qed
.
Lemma
lty_mutex_copyable
A
:
⊢
copyable
(
mutex
A
).
Proof
.
iIntros
(
v
)
"!> #Hv !>"
.
iFrame
"Hv"
.
Qed
.
(* Rules about combining `copy` and other type formers *)
Lemma
lty_prod_copy_comm
A
B
:
⊢
copy
A
*
copy
B
<
:
>
copy
(
A
*
B
).
Proof
.
iSplit
;
iModIntro
;
iIntros
(
v
)
"#Hv"
;
iDestruct
"Hv"
as
(
v1
v2
->)
"[Hv1 Hv2]"
.
-
iModIntro
.
iExists
v1
,
v2
.
iSplit
=>//.
iSplitL
;
iModIntro
;
auto
.
-
iExists
v1
,
v2
.
iSplit
=>//.
iSplit
;
iModIntro
;
iModIntro
;
auto
.
Qed
.
Lemma
lty_sum_copy_comm
A
B
:
⊢
copy
A
+
copy
B
<
:
>
copy
(
A
+
B
).
Proof
.
iSplit
;
iModIntro
;
iIntros
(
v
)
"#Hv"
;
iDestruct
"Hv"
as
"[Hv|Hv]"
;
iDestruct
"Hv"
as
(
w
)
"[Heq Hw]"
;
try
iModIntro
.
-
iLeft
.
iExists
w
.
iFrame
"Heq"
.
iModIntro
.
iApply
"Hw"
.
-
iRight
.
iExists
w
.
iFrame
"Heq"
.
iModIntro
.
iApply
"Hw"
.
-
iLeft
.
iExists
w
.
iFrame
"Heq"
.
iModIntro
.
iModIntro
.
iApply
"Hw"
.
-
iRight
.
iExists
w
.
iFrame
"Heq"
.
iModIntro
.
iModIntro
.
iApply
"Hw"
.
Qed
.
Lemma
lty_exist_copy_comm
F
:
⊢
(
∃
A
,
copy
(
F
A
))
<
:
>
copy
(
∃
A
,
F
A
).
Proof
.
iSplit
;
iModIntro
;
iIntros
(
v
)
"#Hv"
;
iDestruct
"Hv"
as
(
A
)
"Hv"
;
try
iModIntro
;
iExists
A
;
repeat
iModIntro
;
iApply
"Hv"
.
Qed
.
(* TODO(COPY) TODO(VALUERES): Do the forall type former, once we have the value restriction *)
(* Copyability of recursive types *)
Lemma
lty_rec_copy
C
`
{!
Contractive
C
}
:
(
∀
A
,
▷
copyable
A
-
∗
copyable
(
C
A
))
-
∗
copyable
(
lty_rec
C
).
Proof
.
iIntros
"#Hcopy"
.
iL
ö
b
as
"IH"
.
iIntros
(
v
)
"!> Hv"
.
rewrite
/
lty_rec
.
rewrite
{
2
}
fixpoint_unfold
.
iSpecialize
(
"Hcopy"
with
"IH"
).
rewrite
{
3
}/
lty_rec_aux
.
iSpecialize
(
"Hcopy"
with
"Hv"
).
iDestruct
"Hcopy"
as
"#Hcopy"
.
iModIntro
.
iEval
(
rewrite
fixpoint_unfold
).
iApply
"Hcopy"
.
Qed
.
(* TODO: Get rid of side condition that x does not appear in Γ *)
Lemma
env_split_copy
Γ
Γ
1
Γ
2
(
x
:
string
)
A
:
Γ
!!
x
=
None
→
Γ
1
!!
x
=
None
→
Γ
2
!!
x
=
None
→
copyable
A
-
∗
env_split
Γ
Γ
1
Γ
2
-
∗
env_split
(<[
x
:
=
A
]>
Γ
)
(<[
x
:
=
A
]>
Γ
1
)
(<[
x
:
=
A
]>
Γ
2
).
Proof
.
iIntros
(
H
Γ
x
H
Γ
1
x
H
Γ
2
x
)
"#Hcopy #Hsplit"
.
iIntros
(
vs
)
"!>"
.
iSplit
.
-
iIntros
"HΓ"
.
iPoseProof
(
big_sepM_insert
with
"HΓ"
)
as
"[Hv HΓ]"
;
first
by
assumption
.
iDestruct
"Hv"
as
(
v
?)
"HAv2"
.
iDestruct
(
"Hcopy"
with
"HAv2"
)
as
"#HAv"
.
iDestruct
(
"Hsplit"
with
"HΓ"
)
as
"[HΓ1 HΓ2]"
.
iSplitL
"HΓ1"
;
iApply
big_sepM_insert_2
;
simpl
;
eauto
.
-
iIntros
"[HΓ1 HΓ2]"
.
iPoseProof
(
big_sepM_insert
with
"HΓ1"
)
as
"[Hv HΓ1]"
;
first
by
assumption
.
iPoseProof
(
big_sepM_insert
with
"HΓ2"
)
as
"[_ HΓ2]"
;
first
by
assumption
.
iApply
(
big_sepM_insert_2
with
"[Hv]"
)=>
//.
iApply
"Hsplit"
.
iFrame
"HΓ1 HΓ2"
.
Qed
.
Definition
env_copy
(
Γ
Γ
'
:
gmap
string
(
lty
Σ
))
:
iProp
Σ
:
=
(
■
∀
vs
,
env_ltyped
Γ
vs
-
∗
□
env_ltyped
Γ
'
vs
)%
I
.
Lemma
env_copy_empty
:
⊢
env_copy
∅
∅
.
Proof
.
iIntros
(
vs
)
"!> _ !> "
.
by
rewrite
/
env_ltyped
.
Qed
.
Lemma
env_copy_extend
x
A
Γ
Γ
'
:
Γ
!!
x
=
None
→
env_copy
Γ
Γ
'
-
∗
env_copy
(<[
x
:
=
A
]>
Γ
)
Γ
'
.
Proof
.
iIntros
(
H
Γ
)
"#Hcopy"
.
iIntros
(
vs
)
"!> Hvs"
.
rewrite
/
env_ltyped
.
iDestruct
(
big_sepM_insert
with
"Hvs"
)
as
"[_ Hvs]"
;
first
by
assumption
.
iApply
(
"Hcopy"
with
"Hvs"
).
Qed
.
Lemma
env_copy_extend_copy
x
A
Γ
Γ
'
:
Γ
!!
x
=
None
→
Γ
'
!!
x
=
None
→
copyable
A
-
∗
env_copy
Γ
Γ
'
-
∗
env_copy
(<[
x
:
=
A
]>
Γ
)
(<[
x
:
=
A
]>
Γ
'
).
Proof
.
iIntros
(
H
Γ
x
H
Γ
'
x
)
"#HcopyA #Hcopy"
.
iIntros
(
vs
)
"!> Hvs"
.
rewrite
/
env_ltyped
.
iDestruct
(
big_sepM_insert
with
"Hvs"
)
as
"[HA Hvs]"
;
first
done
.
iDestruct
(
"Hcopy"
with
"Hvs"
)
as
"#Hvs'"
.
iDestruct
"HA"
as
(
v
?)
"HA2"
.
iDestruct
(
"HcopyA"
with
"HA2"
)
as
"#HA"
.
iIntros
"!>"
.
iApply
big_sepM_insert
;
first
done
.
iSplitL
;
eauto
.
Qed
.
(* TODO: Maybe move this back to `typing.v` (requires restructuring to avoid
circular dependencies). *)
(* Typing rule for introducing copyable functions *)
Lemma
ltyped_rec
Γ
Γ
'
f
x
e
A1
A2
:
env_copy
Γ
Γ
'
-
∗
(
binder_insert
f
(
A1
→
A2
)%
kind
(
binder_insert
x
A1
Γ
'
)
⊨
e
:
A2
)
-
∗
Γ
⊨
(
rec
:
f
x
:
=
e
)
:
A1
→
A2
⫤
∅
.
Proof
.
iIntros
"#Hcopy #He"
.
iIntros
(
vs
)
"!> HΓ /="
.
iApply
wp_fupd
.
wp_pures
.
iDestruct
(
"Hcopy"
with
"HΓ"
)
as
"HΓ"
.
iMod
(
fupd_mask_mono
with
"HΓ"
)
as
"#HΓ"
;
first
done
.
iModIntro
.
iSplitL
;
last
by
iApply
env_ltyped_empty
.
iL
ö
b
as
"IH"
.
iIntros
(
v
)
"!> HA1"
.
wp_pures
.
set
(
r
:
=
RecV
f
x
_
).
iDestruct
(
"He"
$!(
binder_insert
f
r
(
binder_insert
x
v
vs
))
with
"[HΓ HA1]"
)
as
"He'"
.
{
iApply
(
env_ltyped_insert
with
"IH"
).
iApply
(
env_ltyped_insert
with
"HA1 HΓ"
).
}
iDestruct
(
wp_wand
_
_
_
_
(
λ
v
,
A2
v
)
with
"He' []"
)
as
"He'"
.
{
iIntros
(
w
)
"[$ _]"
.
}
destruct
x
as
[|
x
],
f
as
[|
f
]
;
rewrite
/=
-
?subst_map_insert
//.
destruct
(
decide
(
x
=
f
))
as
[->|].
-
by
rewrite
subst_subst
delete_idemp
!
insert_insert
-
subst_map_insert
.
-
rewrite
subst_subst_ne
//
-
subst_map_insert
.
by
rewrite
-
delete_insert_ne
//
-
subst_map_insert
.
Qed
.
End
copying
.
theories/logrel/
ltyping
.v
→
theories/logrel/
environments
.v
100755 → 100644
View file @
0bc616f0
From
actris
.
logrel
Require
Import
model
.
From
iris
.
heap_lang
Require
Export
lifting
metatheory
.
From
iris
.
base_logic
.
lib
Require
Import
invariants
.
From
iris
.
heap_lang
Require
Import
adequacy
notation
proofmode
.
From
actris
.
logrel
Require
Export
term_types
.
From
iris
.
proofmode
Require
Import
tactics
.
Sec
tion
E
nv
ironment
.
Context
`
{
invG
Σ
}.
Implicit
Types
A
:
lty
Σ
.
Defini
tion
e
nv
_ltyped
{
Σ
}
(
Γ
:
gmap
string
(
ltty
Σ
))
(
vs
:
gmap
string
val
)
:
iProp
Σ
:
=
([
∗
map
]
i
↦
A
∈
Γ
,
∃
v
,
⌜
vs
!!
i
=
Some
v
⌝
∗
ltty_car
A
v
)%
I
.
Definition
env_ltyped
(
Γ
:
gmap
string
(
lty
Σ
))
(
vs
:
gmap
string
val
)
:
iProp
Σ
:
=
([
∗
map
]
i
↦
A
∈
Γ
,
∃
v
,
⌜
vs
!!
i
=
Some
v
⌝
∗
lty_car
A
v
)%
I
.
Definition
env_split
{
Σ
}
(
Γ
Γ
1
Γ
2
:
gmap
string
(
ltty
Σ
))
:
iProp
Σ
:
=
(
■
∀
vs
,
env_ltyped
Γ
vs
∗
-
∗
(
env_ltyped
Γ
1
vs
∗
env_ltyped
Γ
2
vs
))%
I
.
Lemma
env_ltyped_empty
vs
:
⊢
env_ltyped
∅
vs
.
Definition
env_copy
{
Σ
}
(
Γ
Γ
'
:
gmap
string
(
ltty
Σ
))
:
iProp
Σ
:
=
(
■
∀
vs
,
env_ltyped
Γ
vs
-
∗
□
env_ltyped
Γ
'
vs
)%
I
.
Section
env
.
Context
{
Σ
:
gFunctors
}.
Implicit
Types
A
:
ltty
Σ
.
Implicit
Types
Γ
:
gmap
string
(
ltty
Σ
).
Lemma
env_ltyped_empty
vs
:
⊢
@{
iPropI
Σ
}
env_ltyped
∅
vs
.
Proof
.
by
iApply
big_sepM_empty
.
Qed
.
Lemma
env_ltyped_lookup
Γ
vs
x
A
:
Γ
!!
x
=
Some
A
→
env_ltyped
Γ
vs
-
∗
∃
v
,
⌜
vs
!!
x
=
Some
v
⌝
∗
A
v
∗
env_ltyped
(
delete
x
Γ
)
vs
.
env_ltyped
Γ
vs
-
∗
∃
v
,
⌜
vs
!!
x
=
Some
v
⌝
∗
ltty_car
A
v
∗
env_ltyped
(
delete
x
Γ
)
vs
.
Proof
.
iIntros
(
H
Γ
x
)
"HΓ"
.
iPoseProof
(
big_sepM_delete
with
"HΓ"
)
as
"[H1 H2]"
;
eauto
.
iDestruct
"H1"
as
(
v
)
"H1"
.
eauto
with
iFrame
.
iPoseProof
(
big_sepM_delete
with
"HΓ"
)
as
"[HA H]"
;
eauto
.
iDestruct
"HA"
as
(
v
)
"HA"
;
eauto
with
iFrame
.
Qed
.
Lemma
env_ltyped_insert
Γ
vs
x
A
v
:
A
v
-
∗
env_ltyped
Γ
vs
-
∗
ltty_car
A
v
-
∗
env_ltyped
Γ
vs
-
∗
env_ltyped
(
binder_insert
x
A
Γ
)
(
binder_insert
x
v
vs
).
Proof
.
destruct
x
as
[|
x
]=>
/=
;
first
by
auto
.
...
...
@@ -49,9 +55,6 @@ Section Environment.
by
rewrite
-
Hw
lookup_insert_ne
.
Qed
.
Definition
env_split
(
Γ
Γ
1
Γ
2
:
gmap
string
(
lty
Σ
))
:
iProp
Σ
:
=
(
■
∀
vs
,
env_ltyped
Γ
vs
∗
-
∗
(
env_ltyped
Γ
1
vs
∗
env_ltyped
Γ
2
vs
))%
I
.
Lemma
env_split_id_l
Γ
:
⊢
env_split
Γ
∅
Γ
.
Proof
.
iIntros
"!>"
(
vs
).
...
...
@@ -63,7 +66,7 @@ Section Environment.
iSplit
;
[
iIntros
"$"
|
iIntros
"[$ _]"
]
;
iApply
env_ltyped_empty
.
Qed
.
Lemma
env_split_empty
:
⊢
env_split
∅
∅
∅
.
Lemma
env_split_empty
:
⊢
@{
iPropI
Σ
}
env_split
∅
∅
∅
.
Proof
.
iIntros
"!>"
(
vs
).
iSplit
;
[
iIntros
"HΓ"
|
iIntros
"[HΓ1 HΓ2]"
]
;
auto
.
...
...
@@ -107,39 +110,53 @@ Section Environment.
by
iApply
env_split_comm
.
Qed
.
End
Environment
.
(* The semantic typing judgement *)
Definition
ltyped
`
{!
heapG
Σ
}
(
Γ
Γ
'
:
gmap
string
(
lty
Σ
))
(
e
:
expr
)
(
A
:
lty
Σ
)
:
iProp
Σ
:
=
(
■
∀
vs
,
env_ltyped
Γ
vs
-
∗
WP
subst_map
vs
e
{{
v
,
A
v
∗
env_ltyped
Γ
'
vs
}})%
I
.
Notation
"Γ ⊨ e : A ⫤ Γ'"
:
=
(
ltyped
Γ
Γ
'
e
A
)
(
at
level
100
,
e
at
next
level
,
A
at
level
200
).
Notation
"Γ ⊨ e : A"
:
=
(
Γ
⊨
e
:
A
⫤
Γ
)
(
at
level
100
,
e
at
next
level
,
A
at
level
200
).
Lemma
ltyped_frame
`
{!
heapG
Σ
}
(
Γ
Γ
'
Γ
1
Γ
1
'
Γ
2
:
gmap
string
(
lty
Σ
))
e
A
:
env_split
Γ
Γ
1
Γ
2
-
∗
env_split
Γ
'
Γ
1
'
Γ
2
-
∗
(
Γ
1
⊨
e
:
A
⫤
Γ
1
'
)
-
∗
Γ
⊨
e
:
A
⫤
Γ
'
.
Proof
.
iIntros
"#Hsplit #Hsplit' #Htyped !>"
(
vs
)
"Henv"
.
iDestruct
(
"Hsplit"
with
"Henv"
)
as
"[Henv1 Henv2]"
.
iApply
(
wp_wand
with
"(Htyped Henv1)"
).
iIntros
(
v
)
"[$ Henv1']"
.
iApply
"Hsplit'"
.
iFrame
"Henv1' Henv2"
.
Qed
.
Lemma
ltyped_safety
`
{
heapPreG
Σ
}
e
σ
es
σ
'
e'
Γ
'
:
(
∀
`
{
heapG
Σ
},
∃
A
,
⊢
∅
⊨
e
:
A
⫤
Γ
'
)
→
rtc
erased_step
([
e
],
σ
)
(
es
,
σ
'
)
→
e'
∈
es
→
is_Some
(
to_val
e'
)
∨
reducible
e'
σ
'
.
Proof
.
intros
Hty
.
apply
(
heap_adequacy
Σ
NotStuck
e
σ
(
λ
_
,
True
))=>
//
?.
destruct
(
Hty
_
)
as
[
A
He
].
iStartProof
.
iDestruct
(
He
)
as
"He"
.
iSpecialize
(
"He"
$!
∅
).
iSpecialize
(
"He"
with
"[]"
)
;
first
by
rewrite
/
env_ltyped
.
iEval
(
rewrite
-(
subst_map_empty
e
)).
iApply
(
wp_wand
with
"He"
)
;
auto
.
Qed
.
(* TODO: Get rid of side condition that x does not appear in Γ *)
Lemma
env_split_copyable
Γ
Γ
1
Γ
2
(
x
:
string
)
A
:
Γ
!!
x
=
None
→
Γ
1
!!
x
=
None
→
Γ
2
!!
x
=
None
→
lty_copyable
A
-
∗
env_split
Γ
Γ
1
Γ
2
-
∗
env_split
(<[
x
:
=
A
]>
Γ
)
(<[
x
:
=
A
]>
Γ
1
)
(<[
x
:
=
A
]>
Γ
2
).
Proof
.
iIntros
(
H
Γ
x
H
Γ
1
x
H
Γ
2
x
)
"#Hcopy #Hsplit"
.
iIntros
(
vs
)
"!>"
.
iSplit
.
-
iIntros
"HΓ"
.
iPoseProof
(
big_sepM_insert
with
"HΓ"
)
as
"[Hv HΓ]"
;
first
by
assumption
.
iDestruct
"Hv"
as
(
v
?)
"HAv2"
.
iDestruct
(
"Hcopy"
with
"HAv2"
)
as
"#HAv"
.
iDestruct
(
"Hsplit"
with
"HΓ"
)
as
"[HΓ1 HΓ2]"
.
iSplitL
"HΓ1"
;
iApply
big_sepM_insert_2
;
simpl
;
eauto
.
-
iIntros
"[HΓ1 HΓ2]"
.
iPoseProof
(
big_sepM_insert
with
"HΓ1"
)
as
"[Hv HΓ1]"
;
first
by
assumption
.
iPoseProof
(
big_sepM_insert
with
"HΓ2"
)
as
"[_ HΓ2]"
;
first
by
assumption
.
iApply
(
big_sepM_insert_2
with
"[Hv]"
)=>
//.
iApply
"Hsplit"
.
iFrame
"HΓ1 HΓ2"
.
Qed
.
Lemma
env_copy_empty
:
⊢
@{
iPropI
Σ
}
env_copy
∅
∅
.
Proof
.
iIntros
(
vs
)
"!> _ !> "
.
by
rewrite
/
env_ltyped
.
Qed
.
Lemma
env_copy_extend
x
A
Γ
Γ
'
:
Γ
!!
x
=
None
→
env_copy
Γ
Γ
'
-
∗
env_copy
(<[
x
:
=
A
]>
Γ
)
Γ
'
.
Proof
.
iIntros
(
H
Γ
)
"#Hcopy"
.
iIntros
(
vs
)
"!> Hvs"
.
rewrite
/
env_ltyped
.
iDestruct
(
big_sepM_insert
with
"Hvs"
)
as
"[_ Hvs]"
;
first
by
assumption
.
iApply
(
"Hcopy"
with
"Hvs"
).
Qed
.
Lemma
env_copy_extend_copyable
x
A
Γ
Γ
'
:
Γ
!!
x
=
None
→
Γ
'
!!
x
=
None
→
lty_copyable
A
-
∗
env_copy
Γ
Γ
'
-
∗
env_copy
(<[
x
:
=
A
]>
Γ
)
(<[
x
:
=
A
]>
Γ
'
).
Proof
.
iIntros
(
H
Γ
x
H
Γ
'
x
)
"#HcopyA #Hcopy"
.
iIntros
(
vs
)
"!> Hvs"
.
rewrite
/
env_ltyped
.
iDestruct
(
big_sepM_insert
with
"Hvs"
)
as
"[HA Hvs]"
;
first
done
.
iDestruct
(
"Hcopy"
with
"Hvs"
)
as
"#Hvs'"
.
iDestruct
"HA"
as
(
v
?)
"HA2"
.
iDestruct
(
"HcopyA"
with
"HA2"
)
as
"#HA"
.
iIntros
"!>"
.
iApply
big_sepM_insert
;
first
done
.
iSplitL
;
eauto
.
Qed
.
End
env
.
theories/logrel/examples/double.v
View file @
0bc616f0
From
iris
.
heap_lang
Require
Export
lifting
metatheory
.
From
iris
.
base_logic
.
lib
Require
Import
invariants
.
From
iris
.
heap_lang
Require
Import
notation
proofmode
lib
.
par
lib
.
spin_lock
.
From
iris
.
algebra
Require
Import
agree
frac
csum
excl
frac_auth
.
From
actris
.
channel
Require
Import
channel
proto
proofmode
.
From
actris
.
logrel
Require
Export
types
subtyping
.
From
iris
.
algebra
Require
Import
frac
.
From
iris
.
heap_lang
.
lib
Require
Export
par
spin_lock
.
From
actris
.
channel
Require
Import
proofmode
.
From
actris
.
logrel
Require
Export
typing_judgment
session_types
.
From
actris
.
logrel
Require
Import
environments
.
Definition
prog
:
val
:
=
λ
:
"c"
,
let
:
"lock"
:
=
newlock
#()
in
...
...
@@ -19,13 +18,8 @@ Definition prog : val := λ: "c",
"x2"
).
Class
fracG
Σ
:
=
{
frac_inG
:
>
inG
Σ
fracR
}.
Definition
frac
Σ
:
gFunctors
:
=
#[
GFunctor
fracR
].
Instance
subG_frac
Σ
{
Σ
}
:
subG
frac
Σ
Σ
→
fracG
Σ
.
Proof
.
solve_inG
.
Qed
.
Section
double
.
Context
`
{
heapG
Σ
,
chanG
Σ
,
frac
G
Σ
,
spawnG
Σ
}.
Context
`
{
heapG
Σ
,
chanG
Σ
,
inG
Σ
frac
R
,
spawnG
Σ
}.
Definition
prog_prot
:
iProto
Σ
:
=
(<?>
(
x
:
Z
),
MSG
#
x
;
<?>
(
y
:
Z
),
MSG
#
y
;
END
)%
proto
.
...
...
@@ -98,7 +92,7 @@ Section double.
iSplitL
;
last
by
iApply
env_ltyped_empty
.
iIntros
(
c
)
"Hc"
.
iApply
(
wp_prog
with
"[Hc]"
).
{
iApply
(
iProto_mapsto_le
_
(<??>
lty_int
;
<??>
lty_int
;
END
)
%
kind
with
"Hc"
).
{
iApply
(
iProto_mapsto_le
_
(
lsty_car
(<??>
lty_int
;
<??>
lty_int
;
END
)
)
with
"Hc"
).
iApply
iProto_le_recv
.
iIntros
"!> !> !>"
(?
[
x
->]).
iExists
_
.
do
2
(
iSplit
;
[
done
|]).
...
...
theories/logrel/examples/pair.v
View file @
0bc616f0
From
iris
.
heap_lang
Require
Import
notation
proofmode
.
From
actris
.
channel
Require
Import
channel
proto
proofmode
.
From
actris
.
logrel
Require
Export
types
.
From
actris
.
logrel
Require
Export
term_typing_rules
.
From
iris
.
proofmode
Require
Import
tactics
.
Definition
prog
:
expr
:
=
λ
:
"c"
,
(
recv
"c"
,
recv
"c"
).
...
...
@@ -14,5 +13,4 @@ Section pair.
iApply
ltyped_lam
.
iApply
ltyped_pair
.
iApply
ltyped_recv
.
iApply
ltyped_recv
.
Qed
.
End
pair
.
theories/logrel/lsty.v
deleted
100644 → 0
View file @
4e372fb3
From
actris
.
logrel
Require
Export
ltyping
.
From
iris
.
heap_lang
Require
Export
lifting
metatheory
.
From
iris
.
base_logic
.
lib
Require
Import
invariants
.
From
iris
.
heap_lang
Require
Import
notation
proofmode
.
From
actris
.
channel
Require
Import
proto
proofmode
.
Record
lsty
Σ
:
=
Lsty
{
lsty_car
:
>
iProto
Σ
;
}.
Arguments
Lsty
{
_
}
_
%
proto
.
Arguments
lsty_car
{
_
}
_
:
simpl
never
.
Bind
Scope
lsty_scope
with
lsty
.
Delimit
Scope
lsty_scope
with
lsty
.
Section
lsty_ofe
.
Context
`
{
Σ
:
gFunctors
}.
Instance
lsty_equiv
:
Equiv
(
lsty
Σ
)
:
=
λ
P
Q
,
lsty_car
P
≡
lsty_car
Q
.
Instance
lsty_dist
:
Dist
(
lsty
Σ
)
:
=
λ
n
P
Q
,
lsty_car
P
≡
{
n
}
≡
lsty_car
Q
.
Lemma
lsty_ofe_mixin
:
OfeMixin
(
lsty
Σ
).
Proof
.
by
apply
(
iso_ofe_mixin
(
lsty_car
:
_
→
iProto
_
)).
Qed
.
Canonical
Structure
lstyO
:
=
OfeT
(
lsty
Σ
)
lsty_ofe_mixin
.
Global
Instance
lsty_cofe
:
Cofe
lstyO
.
Proof
.
by
apply
(
iso_cofe
(@
Lsty
_
:
_
→
lstyO
)
lsty_car
).
Qed
.
Global
Instance
lsty_inhabited
:
Inhabited
(
lsty
Σ
)
:
=
populate
(
Lsty
inhabitant
).
Global
Instance
lsty_car_ne
:
NonExpansive
lsty_car
.
Proof
.
intros
n
A
A'
H
.
exact
H
.
Qed
.
Global
Instance
lsty_car_proper
:
Proper
((
≡
)
==>
(
≡
))
lsty_car
.
Proof
.
intros
A
A'
H
.
exact
H
.
Qed
.
Global
Instance
Lsty_ne
:
NonExpansive
Lsty
.
Proof
.
solve_proper
.
Qed
.
Global
Instance
Lsty_proper
:
Proper
((
≡
)
==>
(
≡
))
Lsty
.
Proof
.
solve_proper
.
Qed
.
End
lsty_ofe
.
Arguments
lstyO
:
clear
implicits
.
theories/logrel/model.v
View file @
0bc616f0
From
iris
.
heap_lang
Require
Export
lifting
metatheory
.
From
iris
.
base_logic
.
lib
Require
Import
invariants
.
From
iris
.
heap_lang
Require
Import
notation
proofmode
.
From
actris
.
channel
Require
Import
proto
proofmode
.
Record
lty_raw
Σ
:
=
Lty
{
lty_car
:
>
val
→
iProp
Σ
;