Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
A
Actris
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
5
Issues
5
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Iris
Actris
Commits
76e934c0
Commit
76e934c0
authored
May 06, 2020
by
Daniël Louwrink
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'daniel/update_typing_rules' into 'master'
Update typing rules See merge request
!15
parents
01ec9471
35a4e878
Pipeline
#27733
failed with stage
in 4 minutes and 34 seconds
Changes
6
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
6 changed files
with
409 additions
and
394 deletions
+409
-394
_CoqProject
_CoqProject
+1
-0
theories/logrel/lib/mutex.v
theories/logrel/lib/mutex.v
+145
-0
theories/logrel/subtyping_rules.v
theories/logrel/subtyping_rules.v
+2
-29
theories/logrel/term_types.v
theories/logrel/term_types.v
+5
-34
theories/logrel/term_typing_judgment.v
theories/logrel/term_typing_judgment.v
+0
-13
theories/logrel/term_typing_rules.v
theories/logrel/term_typing_rules.v
+256
-318
No files found.
_CoqProject
View file @
76e934c0
...
...
@@ -27,5 +27,6 @@ theories/logrel/operators.v
theories/logrel/term_typing_judgment.v
theories/logrel/subtyping_rules.v
theories/logrel/term_typing_rules.v
theories/logrel/lib/mutex.v
theories/logrel/examples/double.v
theories/logrel/examples/pair.v
theories/logrel/lib/mutex.v
0 → 100644
View file @
76e934c0
From
iris
.
base_logic
.
lib
Require
Import
invariants
.
From
iris
.
heap_lang
Require
Export
spin_lock
.
From
actris
.
logrel
Require
Export
term_types
term_typing_judgment
subtyping
.
From
actris
.
logrel
Require
Import
environments
.
From
actris
.
channel
Require
Import
proofmode
.
From
iris
.
heap_lang
Require
Import
metatheory
.
(** Mutex functions *)
Definition
mutex_alloc
:
val
:
=
λ
:
"x"
,
(
newlock
#(),
ref
"x"
).
Definition
mutex_acquire
:
val
:
=
λ
:
"x"
,
acquire
(
Fst
"x"
)
;;
!
(
Snd
"x"
).
Definition
mutex_release
:
val
:
=
λ
:
"guard"
"inner"
,
Snd
"guard"
<-
"inner"
;;
release
(
Fst
"guard"
).
(** Semantic types *)
Definition
lty_mutex
`
{
heapG
Σ
,
lockG
Σ
}
(
A
:
ltty
Σ
)
:
ltty
Σ
:
=
Ltty
(
λ
w
,
∃
(
γ
:
gname
)
(
l
:
loc
)
(
lk
:
val
),
⌜
w
=
PairV
lk
#
l
⌝
∗
is_lock
γ
lk
(
∃
v_inner
,
l
↦
v_inner
∗
ltty_car
A
v_inner
))%
I
.
Definition
lty_mutex_guard
`
{
heapG
Σ
,
lockG
Σ
}
(
A
:
ltty
Σ
)
:
ltty
Σ
:
=
Ltty
(
λ
w
,
∃
(
γ
:
gname
)
(
l
:
loc
)
(
lk
:
val
)
(
v
:
val
),
⌜
w
=
PairV
lk
#
l
⌝
∗
is_lock
γ
lk
(
∃
v_inner
,
l
↦
v_inner
∗
ltty_car
A
v_inner
)
∗
spin_lock
.
locked
γ
∗
l
↦
v
)%
I
.
Instance
:
Params
(@
lty_mutex
)
3
:
=
{}.
Instance
:
Params
(@
lty_mutex_guard
)
3
:
=
{}.
Notation
"'mutex' A"
:
=
(
lty_mutex
A
)
(
at
level
10
)
:
lty_scope
.
Notation
"'mutex_guard' A"
:
=
(
lty_mutex_guard
A
)
(
at
level
10
)
:
lty_scope
.
Section
properties
.
Context
`
{
heapG
Σ
,
lockG
Σ
}.
Implicit
Types
A
:
ltty
Σ
.
Global
Instance
lty_mutex_contractive
:
Contractive
lty_mutex
.
Proof
.
solve_contractive
.
Qed
.
Global
Instance
lty_mutex_ne
:
NonExpansive
lty_mutex
.
Proof
.
solve_proper
.
Qed
.
Global
Instance
lty_mutex_guard_contractive
:
Contractive
lty_mutex_guard
.
Proof
.
solve_contractive
.
Qed
.
Global
Instance
lty_mutex_guard_ne
:
NonExpansive
lty_mutex_guard
.
Proof
.
solve_proper
.
Qed
.
Lemma
lty_le_mutex
A1
A2
:
▷
(
A1
<
:
>
A2
)
-
∗
mutex
A1
<
:
mutex
A2
.
Proof
.
iIntros
"#[Hle1 Hle2]"
(
v
)
"!>"
.
iDestruct
1
as
(
γ
l
lk
->)
"Hinv"
.
iExists
γ
,
l
,
lk
.
iSplit
;
first
done
.
iApply
(
spin_lock
.
is_lock_iff
with
"Hinv"
).
iIntros
"!> !>"
.
iSplit
.
-
iDestruct
1
as
(
v
)
"[Hl HA]"
.
iExists
v
.
iFrame
"Hl"
.
by
iApply
"Hle1"
.
-
iDestruct
1
as
(
v
)
"[Hl HA]"
.
iExists
v
.
iFrame
"Hl"
.
by
iApply
"Hle2"
.
Qed
.
Lemma
lty_copyable_mutex
A
:
⊢
lty_copyable
(
mutex
A
).
Proof
.
iIntros
(
v
)
"!> #Hv !>"
.
iFrame
"Hv"
.
Qed
.
Lemma
lty_le_mutex_guard
A1
A2
:
▷
(
A1
<
:
>
A2
)
-
∗
mutex_guard
A1
<
:
mutex_guard
A2
.
Proof
.
iIntros
"#[Hle1 Hle2]"
(
v
)
"!>"
.
iDestruct
1
as
(
γ
l
lk
w
->)
"[Hinv [Hlock Hinner]]"
.
iExists
γ
,
l
,
lk
,
w
.
iSplit
;
first
done
.
iFrame
"Hlock Hinner"
.
iApply
(
spin_lock
.
is_lock_iff
with
"Hinv"
).
iIntros
"!> !>"
.
iSplit
.
-
iDestruct
1
as
(
v
)
"[Hl HA]"
.
iExists
v
.
iFrame
"Hl"
.
by
iApply
"Hle1"
.
-
iDestruct
1
as
(
v
)
"[Hl HA]"
.
iExists
v
.
iFrame
"Hl"
.
by
iApply
"Hle2"
.
Qed
.
End
properties
.
Section
rules
.
Context
`
{
heapG
Σ
,
lockG
Σ
}.
(** Mutex properties *)
Lemma
ltyped_mutex_alloc
A
:
⊢
∅
⊨
mutex_alloc
:
A
→
mutex
A
.
Proof
.
iIntros
(
vs
)
"!> HΓ /="
.
iApply
wp_value
.
iSplitL
;
last
by
iApply
env_ltyped_empty
.
iIntros
"!>"
(
v
)
"Hv"
.
rewrite
/
mutex_alloc
.
wp_pures
.
wp_alloc
l
as
"Hl"
.
wp_bind
(
newlock
_
).
set
(
N
:
=
nroot
.@
"makelock"
).
iAssert
(
∃
inner
,
l
↦
inner
∗
ltty_car
A
inner
)%
I
with
"[Hl Hv]"
as
"Hlock"
.
{
iExists
v
.
iFrame
"Hl Hv"
.
}
wp_apply
(
newlock_spec
with
"Hlock"
).
iIntros
(
lk
γ
)
"Hlock"
.
wp_pures
.
iExists
γ
,
l
,
lk
.
iSplit
=>
//.
Qed
.
Lemma
ltyped_mutex_acquire
Γ
(
x
:
string
)
A
:
Γ
!!
x
=
Some
(
mutex
A
)%
lty
→
⊢
Γ
⊨
mutex_acquire
x
:
A
⫤
<[
x
:
=
(
mutex_guard
A
)%
lty
]>
Γ
.
Proof
.
iIntros
(
Hx
vs
)
"!> HΓ /="
.
iDestruct
(
env_ltyped_lookup
with
"HΓ"
)
as
(
v
Hv
)
"[HA HΓ]"
;
first
done
;
rewrite
Hv
.
rewrite
/
mutex_acquire
.
wp_pures
.
iDestruct
"HA"
as
(
γ
l
lk
->)
"#Hlock"
.
wp_bind
(
acquire
_
).
wp_apply
(
acquire_spec
with
"Hlock"
).
iIntros
"[Hlocked Hinner]"
.
iDestruct
"Hinner"
as
(
v
)
"[Hl HA]"
.
wp_pures
.
wp_load
.
iFrame
"HA"
.
iAssert
(
ltty_car
(
mutex_guard
A
)%
lty
(
lk
,
#
l
))
with
"[Hlocked Hl]"
as
"Hguard"
.
{
iExists
γ
,
l
,
lk
,
v
.
iSplit
=>//.
iFrame
"Hlocked Hl Hlock"
.
}
iDestruct
(
env_ltyped_insert
_
_
x
with
"Hguard HΓ"
)
as
"HΓ"
.
rewrite
/
binder_insert
insert_delete
(
insert_id
_
_
_
Hv
).
iFrame
"HΓ"
.
Qed
.
Lemma
ltyped_mutex_release
Γ
Γ
'
(
x
:
string
)
e
A
:
Γ
'
!!
x
=
Some
(
mutex_guard
A
)%
lty
→
(
Γ
⊨
e
:
A
⫤
Γ
'
)
-
∗
Γ
⊨
mutex_release
x
e
:
()
⫤
<[
x
:
=
(
mutex
A
)%
lty
]>
Γ
'
.
Proof
.
iIntros
(
Hx
)
"#He"
.
iIntros
(
vs
)
"!> HΓ /="
.
wp_bind
(
subst_map
vs
e
).
iApply
(
wp_wand
with
"(He HΓ)"
).
iIntros
(
v
)
"[HA HΓ']"
.
iDestruct
(
env_ltyped_lookup
with
"HΓ'"
)
as
(
g
Hg
)
"[Hguard HΓ']"
;
first
done
;
rewrite
Hg
.
iDestruct
"Hguard"
as
(
γ
l
lk
inner
->)
"(#Hlock & Hlocked & Hinner)"
.
rewrite
/
mutex_release
.
wp_pures
.
wp_store
.
wp_pures
.
iAssert
(
∃
inner
,
l
↦
inner
∗
ltty_car
A
inner
)%
I
with
"[Hinner HA]"
as
"Hinner"
.
{
iExists
v
.
iFrame
"Hinner HA"
.
}
wp_apply
(
release_spec
γ
_
(
∃
inner
,
l
↦
inner
∗
ltty_car
A
inner
)%
I
with
"[Hlocked Hinner]"
).
{
iFrame
"Hlock Hlocked"
.
iDestruct
"Hinner"
as
(
w
)
"[Hl HA]"
.
eauto
with
iFrame
.
}
iIntros
"_"
.
wp_pures
.
iSplit
=>
//.
iAssert
(
ltty_car
(
mutex
A
)%
lty
(
lk
,
#
l
))
with
"[Hlock]"
as
"Hmutex"
.
{
iExists
γ
,
l
,
lk
.
iSplit
=>//.
}
iDestruct
(
env_ltyped_insert
_
_
x
with
"Hmutex HΓ'"
)
as
"HΓ'"
.
rewrite
/
binder_insert
insert_delete
(
insert_id
_
_
_
Hg
).
iFrame
"HΓ'"
.
Qed
.
End
rules
.
theories/logrel/subtyping_rules.v
View file @
76e934c0
...
...
@@ -171,7 +171,7 @@ Section subtyping_rules.
Qed
.
Lemma
lty_le_exist
C1
C2
:
▷
(
∀
A
,
C1
A
<
:
C2
A
)
-
∗
(
∀
A
,
C1
A
<
:
C2
A
)
-
∗
(
∃
A
,
C1
A
)
<
:
(
∃
A
,
C2
A
).
Proof
.
iIntros
"#Hle"
(
v
)
"!>"
.
iDestruct
1
as
(
A
)
"H"
.
iExists
A
.
by
iApply
"Hle"
.
...
...
@@ -187,7 +187,7 @@ Section subtyping_rules.
Qed
.
Lemma
lty_copyable_exist
(
C
:
ltty
Σ
→
ltty
Σ
)
:
▷
(
∀
M
,
lty_copyable
(
C
M
))
-
∗
lty_copyable
(
lty_exist
C
).
(
∀
M
,
lty_copyable
(
C
M
))
-
∗
lty_copyable
(
lty_exist
C
).
Proof
.
iIntros
"#Hle"
.
rewrite
/
lty_copyable
/
tc_opaque
.
iApply
lty_le_r
;
last
by
iApply
lty_le_exist_copy
.
...
...
@@ -236,33 +236,6 @@ Section subtyping_rules.
⊢
lty_copyable
(
ref_shr
A
).
Proof
.
iIntros
(
v
)
"!> #Hv !>"
.
iFrame
"Hv"
.
Qed
.
Lemma
lty_le_mutex
A1
A2
:
▷
(
A1
<
:
>
A2
)
-
∗
mutex
A1
<
:
mutex
A2
.
Proof
.
iIntros
"#[Hle1 Hle2]"
(
v
)
"!>"
.
iDestruct
1
as
(
γ
l
lk
->)
"Hinv"
.
iExists
γ
,
l
,
lk
.
iSplit
;
first
done
.
iApply
(
spin_lock
.
is_lock_iff
with
"Hinv"
).
iIntros
"!> !>"
.
iSplit
.
-
iDestruct
1
as
(
v
)
"[Hl HA]"
.
iExists
v
.
iFrame
"Hl"
.
by
iApply
"Hle1"
.
-
iDestruct
1
as
(
v
)
"[Hl HA]"
.
iExists
v
.
iFrame
"Hl"
.
by
iApply
"Hle2"
.
Qed
.
Lemma
lty_copyable_mutex
A
:
⊢
lty_copyable
(
mutex
A
).
Proof
.
iIntros
(
v
)
"!> #Hv !>"
.
iFrame
"Hv"
.
Qed
.
Lemma
lty_le_mutexguard
A1
A2
:
▷
(
A1
<
:
>
A2
)
-
∗
mutexguard
A1
<
:
mutexguard
A2
.
Proof
.
iIntros
"#[Hle1 Hle2]"
(
v
)
"!>"
.
iDestruct
1
as
(
γ
l
lk
w
->)
"[Hinv [Hlock Hinner]]"
.
iExists
γ
,
l
,
lk
,
w
.
iSplit
;
first
done
.
iFrame
"Hlock Hinner"
.
iApply
(
spin_lock
.
is_lock_iff
with
"Hinv"
).
iIntros
"!> !>"
.
iSplit
.
-
iDestruct
1
as
(
v
)
"[Hl HA]"
.
iExists
v
.
iFrame
"Hl"
.
by
iApply
"Hle1"
.
-
iDestruct
1
as
(
v
)
"[Hl HA]"
.
iExists
v
.
iFrame
"Hl"
.
by
iApply
"Hle2"
.
Qed
.
Lemma
lty_le_chan
S1
S2
:
▷
(
S1
<
:
S2
)
-
∗
chan
S1
<
:
chan
S2
.
...
...
theories/logrel/term_types.v
View file @
76e934c0
...
...
@@ -7,7 +7,7 @@ From actris.channel Require Export channel.
Definition
lty_any
{
Σ
}
:
ltty
Σ
:
=
Ltty
(
λ
w
,
True
%
I
).
Definition
lty_copy
{
Σ
}
(
A
:
ltty
Σ
)
:
ltty
Σ
:
=
Ltty
(
λ
w
,
□
ltty_car
A
w
)%
I
.
Definition
lty_copy_
inv
{
Σ
}
(
A
:
ltty
Σ
)
:
ltty
Σ
:
=
Ltty
(
λ
w
,
coreP
(
ltty_car
A
w
)).
Definition
lty_copy_
minus
{
Σ
}
(
A
:
ltty
Σ
)
:
ltty
Σ
:
=
Ltty
(
λ
w
,
coreP
(
ltty_car
A
w
)).
Definition
lty_copyable
{
Σ
}
(
A
:
ltty
Σ
)
:
iProp
Σ
:
=
tc_opaque
(
A
<
:
lty_copy
A
)%
I
.
...
...
@@ -27,7 +27,7 @@ Definition lty_sum {Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
Definition
lty_forall
`
{
heapG
Σ
}
{
k
}
(
C
:
lty
Σ
k
→
ltty
Σ
)
:
ltty
Σ
:
=
Ltty
(
λ
w
,
∀
A
,
WP
w
#()
{{
ltty_car
(
C
A
)
}})%
I
.
Definition
lty_exist
{
Σ
k
}
(
C
:
lty
Σ
k
→
ltty
Σ
)
:
ltty
Σ
:
=
Ltty
(
λ
w
,
∃
A
,
▷
ltty_car
(
C
A
)
w
)%
I
.
Ltty
(
λ
w
,
∃
A
,
ltty_car
(
C
A
)
w
)%
I
.
Definition
lty_ref_mut
`
{
heapG
Σ
}
(
A
:
ltty
Σ
)
:
ltty
Σ
:
=
Ltty
(
λ
w
,
∃
(
l
:
loc
)
(
v
:
val
),
⌜
w
=
#
l
⌝
∗
l
↦
v
∗
▷
ltty_car
A
v
)%
I
.
...
...
@@ -35,21 +35,11 @@ Definition ref_shrN := nroot .@ "shr_ref".
Definition
lty_ref_shr
`
{
heapG
Σ
}
(
A
:
ltty
Σ
)
:
ltty
Σ
:
=
Ltty
(
λ
w
,
∃
l
:
loc
,
⌜
w
=
#
l
⌝
∗
inv
(
ref_shrN
.@
l
)
(
∃
v
,
l
↦
v
∗
ltty_car
A
v
))%
I
.
Definition
lty_mutex
`
{
heapG
Σ
,
lockG
Σ
}
(
A
:
ltty
Σ
)
:
ltty
Σ
:
=
Ltty
(
λ
w
,
∃
(
γ
:
gname
)
(
l
:
loc
)
(
lk
:
val
),
⌜
w
=
PairV
lk
#
l
⌝
∗
is_lock
γ
lk
(
∃
v_inner
,
l
↦
v_inner
∗
ltty_car
A
v_inner
))%
I
.
Definition
lty_mutexguard
`
{
heapG
Σ
,
lockG
Σ
}
(
A
:
ltty
Σ
)
:
ltty
Σ
:
=
Ltty
(
λ
w
,
∃
(
γ
:
gname
)
(
l
:
loc
)
(
lk
:
val
)
(
v
:
val
),
⌜
w
=
PairV
lk
#
l
⌝
∗
is_lock
γ
lk
(
∃
v_inner
,
l
↦
v_inner
∗
ltty_car
A
v_inner
)
∗
spin_lock
.
locked
γ
∗
l
↦
v
)%
I
.
Definition
lty_chan
`
{
heapG
Σ
,
chanG
Σ
}
(
P
:
lsty
Σ
)
:
ltty
Σ
:
=
Ltty
(
λ
w
,
w
↣
lsty_car
P
)%
I
.
Instance
:
Params
(@
lty_copy
)
1
:
=
{}.
Instance
:
Params
(@
lty_copy_
inv
)
1
:
=
{}.
Instance
:
Params
(@
lty_copy_
minus
)
1
:
=
{}.
Instance
:
Params
(@
lty_copyable
)
1
:
=
{}.
Instance
:
Params
(@
lty_arr
)
2
:
=
{}.
Instance
:
Params
(@
lty_prod
)
1
:
=
{}.
...
...
@@ -58,14 +48,12 @@ Instance: Params (@lty_forall) 2 := {}.
Instance
:
Params
(@
lty_sum
)
1
:
=
{}.
Instance
:
Params
(@
lty_ref_mut
)
2
:
=
{}.
Instance
:
Params
(@
lty_ref_shr
)
2
:
=
{}.
Instance
:
Params
(@
lty_mutex
)
3
:
=
{}.
Instance
:
Params
(@
lty_mutexguard
)
3
:
=
{}.
Instance
:
Params
(@
lty_chan
)
3
:
=
{}.
Notation
any
:
=
lty_any
.
Notation
"()"
:
=
lty_unit
:
lty_scope
.
Notation
"'copy' A"
:
=
(
lty_copy
A
)
(
at
level
10
)
:
lty_scope
.
Notation
"'copy-' A"
:
=
(
lty_copy_
inv
A
)
(
at
level
10
)
:
lty_scope
.
Notation
"'copy-' A"
:
=
(
lty_copy_
minus
A
)
(
at
level
10
)
:
lty_scope
.
Notation
"A ⊸ B"
:
=
(
lty_arr
A
B
)
(
at
level
99
,
B
at
level
200
,
right
associativity
)
:
lty_scope
.
...
...
@@ -81,9 +69,6 @@ Notation "∃ A1 .. An , C" :=
Notation
"'ref_mut' A"
:
=
(
lty_ref_mut
A
)
(
at
level
10
)
:
lty_scope
.
Notation
"'ref_shr' A"
:
=
(
lty_ref_shr
A
)
(
at
level
10
)
:
lty_scope
.
Notation
"'mutex' A"
:
=
(
lty_mutex
A
)
(
at
level
10
)
:
lty_scope
.
Notation
"'mutexguard' A"
:
=
(
lty_mutexguard
A
)
(
at
level
10
)
:
lty_scope
.
Notation
"'chan' A"
:
=
(
lty_chan
A
)
(
at
level
10
)
:
lty_scope
.
Section
term_types
.
...
...
@@ -92,7 +77,7 @@ Section term_types.
Global
Instance
lty_copy_ne
:
NonExpansive
(@
lty_copy
Σ
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
lty_copy_
inv_ne
:
NonExpansive
(@
lty_copy_inv
Σ
).
Global
Instance
lty_copy_
minus_ne
:
NonExpansive
(@
lty_copy_minus
Σ
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
lty_copyable_plain
A
:
Plain
(
lty_copyable
A
).
...
...
@@ -130,9 +115,6 @@ Section term_types.
Global
Instance
lty_forall_ne
`
{
heapG
Σ
}
k
n
:
Proper
(
pointwise_relation
_
(
dist
n
)
==>
dist
n
)
(@
lty_forall
Σ
_
k
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
lty_exist_contractive
k
n
:
Proper
(
pointwise_relation
_
(
dist_later
n
)
==>
dist
n
)
(@
lty_exist
Σ
k
).
Proof
.
solve_contractive
.
Qed
.
Global
Instance
lty_exist_ne
k
n
:
Proper
(
pointwise_relation
_
(
dist
n
)
==>
dist
n
)
(@
lty_exist
Σ
k
).
Proof
.
solve_proper
.
Qed
.
...
...
@@ -147,17 +129,6 @@ Section term_types.
Global
Instance
lty_ref_shr_ne
`
{
heapG
Σ
}
:
NonExpansive
lty_ref_shr
.
Proof
.
solve_proper
.
Qed
.
Global
Instance
lty_mutex_contractive
`
{
heapG
Σ
,
lockG
Σ
}
:
Contractive
lty_mutex
.
Proof
.
solve_contractive
.
Qed
.
Global
Instance
lty_mutex_ne
`
{
heapG
Σ
,
lockG
Σ
}
:
NonExpansive
lty_mutex
.
Proof
.
solve_proper
.
Qed
.
Global
Instance
lty_mutexguard_contractive
`
{
heapG
Σ
,
lockG
Σ
}
:
Contractive
lty_mutexguard
.
Proof
.
solve_contractive
.
Qed
.
Global
Instance
lty_mutexguard_ne
`
{
heapG
Σ
,
lockG
Σ
}
:
NonExpansive
lty_mutexguard
.
Proof
.
solve_proper
.
Qed
.
Global
Instance
lty_chan_ne
`
{
heapG
Σ
,
chanG
Σ
}
:
NonExpansive
lty_chan
.
Proof
.
solve_proper
.
Qed
.
End
term_types
.
theories/logrel/term_typing_judgment.v
View file @
76e934c0
...
...
@@ -14,19 +14,6 @@ Notation "Γ ⊨ e : A ⫤ Γ'" := (ltyped Γ Γ' e A)
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
(
ltty
Σ
))
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
→
...
...
theories/logrel/term_typing_rules.v
View file @
76e934c0
...
...
@@ -14,16 +14,32 @@ Section properties.
Implicit
Types
S
T
:
lsty
Σ
.
Implicit
Types
Γ
:
gmap
string
(
ltty
Σ
).
(** Frame rule *)
Lemma
ltyped_frame
Γ
Γ
'
Γ
1
Γ
1
'
Γ
2
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
.
(** Variable properties *)
Lemma
ltyped_var
Γ
(
x
:
string
)
A
:
Γ
!!
x
=
Some
A
→
⊢
Γ
⊨
x
:
A
⫤
<[
x
:
=
copy
-
A
]>%
lty
Γ
.
Γ
!!
x
=
Some
A
→
⊢
Γ
⊨
x
:
A
⫤
<[
x
:
=
(
copy
-
A
)%
lty
]>
Γ
.
Proof
.
iIntros
(
H
Γ
x
)
"!>"
;
iIntros
(
vs
)
"HΓ /="
.
iDestruct
(
env_ltyped_lookup
with
"HΓ"
)
as
(
v
Hx
)
"[HA HΓ]"
;
first
done
.
rewrite
Hx
.
iApply
wp_value
.
iDestruct
(
coreP_intro
with
"HA"
)
as
"#HAc"
.
iFrame
"HA"
.
iEval
(
rewrite
-
insert_delete
-(
insert_id
vs
x
v
)
//).
by
iApply
(
env_ltyped_insert
_
_
x
).
iDestruct
(
env_ltyped_lookup
with
"HΓ"
)
as
(
v
Hv
)
"[HA HΓ]"
;
first
done
;
rewrite
Hv
.
iApply
wp_value
.
iAssert
(
ltty_car
(
copy
-
A
)
v
)%
lty
as
"#HAm"
.
{
iApply
coreP_intro
.
iApply
"HA"
.
}
iFrame
"HA"
.
iDestruct
(
env_ltyped_insert
_
_
x
with
"HAm HΓ"
)
as
"HΓ"
.
rewrite
/
binder_insert
insert_delete
(
insert_id
_
_
_
Hv
).
iApply
"HΓ"
.
Qed
.
(** Subtyping *)
...
...
@@ -71,9 +87,9 @@ Section properties.
Qed
.
(* Typing rule for introducing copyable functions *)
Lemma
ltyped_rec
Γ
Γ
'
f
x
e
A1
A2
:
Lemma
ltyped_rec
Γ
Γ
'
Γ
''
f
x
e
A1
A2
:
env_copy
Γ
Γ
'
-
∗
(
binder_insert
f
(
A1
→
A2
)%
lty
(
binder_insert
x
A1
Γ
'
)
⊨
e
:
A2
)
-
∗
(
binder_insert
f
(
A1
→
A2
)%
lty
(
binder_insert
x
A1
Γ
'
)
⊨
e
:
A2
⫤
Γ
''
)
-
∗
Γ
⊨
(
rec
:
f
x
:
=
e
)
:
A1
→
A2
⫤
∅
.
Proof
.
iIntros
"#Hcopy #He"
.
iIntros
(
vs
)
"!> HΓ /="
.
iApply
wp_fupd
.
wp_pures
.
...
...
@@ -112,45 +128,6 @@ Section properties.
iApply
env_ltyped_delete
=>
//.
Qed
.
Fixpoint
lty_arr_list
(
As
:
list
(
ltty
Σ
))
(
B
:
ltty
Σ
)
:
ltty
Σ
:
=
match
As
with
|
[]
=>
B
|
A
::
As
=>
A
⊸
lty_arr_list
As
B
end
.
Lemma
lty_arr_list_spec_step
A
As
(
e
:
expr
)
B
ws
y
i
:
(
∀
v
,
ltty_car
A
v
-
∗
WP
subst_map
(<[
y
+
:
+
pretty
i
:
=
v
]>
ws
)
(
switch_lams
y
(
S
i
)
(
length
As
)
e
)
{{
ltty_car
(
lty_arr_list
As
B
)
}})
-
∗
WP
subst_map
ws
(
switch_lams
y
i
(
S
(
length
As
))
e
)
{{
ltty_car
(
lty_arr_list
(
A
::
As
)
B
)
}}.
Proof
.
iIntros
"H"
.
wp_pures
.
iIntros
(
v
)
"HA"
.
iDestruct
(
"H"
with
"HA"
)
as
"H"
.
rewrite
subst_map_insert
.
wp_apply
"H"
.
Qed
.
Lemma
lty_arr_list_spec
As
(
e
:
expr
)
B
ws
y
i
n
:
n
=
length
As
→
(
∀
vs
,
([
∗
list
]
A
;
v
∈
As
;
vs
,
ltty_car
A
v
)
-
∗
WP
subst_map
(
map_string_seq
y
i
vs
∪
ws
)
e
{{
ltty_car
B
}})
-
∗
WP
subst_map
ws
(
switch_lams
y
i
n
e
)
{{
ltty_car
(
lty_arr_list
As
B
)
}}.
Proof
.
iIntros
(
Hlen
)
"H"
.
iInduction
As
as
[|
A
As
]
"IH"
forall
(
ws
i
e
n
Hlen
)
;
simplify_eq
/=.
-
iDestruct
(
"H"
$!
[]
with
"[$]"
)
as
"H"
=>
/=.
by
rewrite
left_id_L
.
-
iApply
lty_arr_list_spec_step
.
iIntros
(
v
)
"HA"
.
iApply
(
"IH"
with
"[//]"
).
iIntros
(
vs
)
"HAs"
.
iSpecialize
(
"H"
$!
(
v
::
vs
))
;
simpl
.
do
2
rewrite
insert_union_singleton_l
.
rewrite
(
map_union_comm
({[
y
+
:
+
pretty
i
:
=
v
]}))
;
last
first
.
{
apply
map_disjoint_singleton_l_2
.
apply
lookup_map_string_seq_None_lt
.
eauto
.
}
rewrite
assoc_L
.
iApply
(
"H"
with
"[$HA $HAs]"
).
Qed
.
(** Product properties *)
Lemma
ltyped_pair
Γ
1
Γ
2
Γ
3 e1
e2
A1
A2
:
(
Γ
2
⊨
e1
:
A1
⫤
Γ
3
)
-
∗
(
Γ
1
⊨
e2
:
A2
⫤
Γ
2
)
-
∗
...
...
@@ -162,19 +139,38 @@ Section properties.
wp_pures
.
iFrame
"HΓ"
.
iExists
w1
,
w2
.
by
iFrame
.
Qed
.
Definition
split
:
val
:
=
λ
:
"pair"
"f"
,
"f"
(
Fst
"pair"
)
(
Snd
"pair"
).
Lemma
ltyped_fst
Γ
A1
A2
(
x
:
string
)
:
Γ
!!
x
=
Some
(
A1
*
A2
)%
lty
→
⊢
Γ
⊨
Fst
x
:
A1
⫤
<[
x
:
=
(
copy
-
A1
*
A2
)%
lty
]>
Γ
.
Proof
.
iIntros
(
Hx
vs
)
"!> HΓ /="
.
iDestruct
(
env_ltyped_lookup
with
"HΓ"
)
as
(
v
Hv
)
"[HA HΓ]"
;
first
done
;
rewrite
Hv
.
iDestruct
"HA"
as
(
v1
v2
->)
"[HA1 HA2]"
.
wp_pures
.
iAssert
(
ltty_car
(
copy
-
A1
)
v1
)%
lty
as
"#HA1m"
.
{
iApply
coreP_intro
.
iApply
"HA1"
.
}
iFrame
"HA1"
.
iAssert
(
ltty_car
(
copy
-
A1
*
A2
)
(
v1
,
v2
))%
lty
with
"[HA2]"
as
"HA"
.
{
iExists
v1
,
v2
.
iSplit
=>//.
iFrame
"HA1m HA2"
.
}
iDestruct
(
env_ltyped_insert
_
_
x
with
"HA HΓ"
)
as
"HΓ"
.
rewrite
/
binder_insert
insert_delete
(
insert_id
_
_
_
Hv
).
iFrame
"HΓ"
.
Qed
.
Lemma
ltyped_split
A1
A2
B
:
⊢
∅
⊨
split
:
A1
*
A2
→
(
A1
⊸
A2
⊸
B
)
⊸
B
.
Lemma
ltyped_snd
Γ
A1
A2
(
x
:
string
)
:
Γ
!!
x
=
Some
(
A1
*
A2
)%
lty
→
⊢
Γ
⊨
Snd
x
:
A2
⫤
<[
x
:
=
(
A1
*
copy
-
A2
)%
lty
]>
Γ
.
Proof
.
iIntros
(
vs
)
"!> HΓ /="
.
iApply
wp_value
.
iSplitL
;
last
by
iApply
env_ltyped_empty
.
iIntros
"!>"
(
v
)
"Hv"
.
rewrite
/
split
.
wp_pures
.
iDestruct
"Hv"
as
(
w1
w2
->)
"[Hw1 Hw2]"
.
iIntros
(
f
)
"Hf"
.
wp_pures
.
iPoseProof
(
"Hf"
with
"Hw1"
)
as
"Hf"
.
wp_apply
(
wp_wand
with
"Hf"
).
iIntros
(
g
)
"Hg"
.
iApply
(
"Hg"
with
"Hw2"
).
iIntros
(
Hx
vs
)
"!> HΓ /="
.
iDestruct
(
env_ltyped_lookup
with
"HΓ"
)
as
(
v
Hv
)
"[HA HΓ]"
;
first
done
;
rewrite
Hv
.
iDestruct
"HA"
as
(
v1
v2
->)
"[HA1 HA2]"
.
wp_pures
.
iAssert
(
ltty_car
(
copy
-
A2
)
v2
)%
lty
as
"#HA2m"
.
{
iApply
coreP_intro
.
iApply
"HA2"
.
}
iFrame
"HA2"
.
iAssert
(
ltty_car
(
A1
*
copy
-
A2
)
(
v1
,
v2
))%
lty
with
"[HA1]"
as
"HA"
.
{
iExists
v1
,
v2
.
iSplit
=>//.
iFrame
"HA2m HA1"
.
}
iDestruct
(
env_ltyped_insert
_
_
x
with
"HA HΓ"
)
as
"HΓ"
.
rewrite
/
binder_insert
insert_delete
(
insert_id
_
_
_
Hv
).
iFrame
"HΓ"
.
Qed
.
(** Sum Properties *)
...
...
@@ -196,24 +192,27 @@ Section properties.
iRight
.
iExists
v
.
auto
.
Qed
.
Definition
paircase
:
val
:
=
λ
:
"pair"
"left"
"right"
,
Case
"pair"
"left"
"right"
.
Lemma
ltyped_paircase
A1
A2
B
:
⊢
∅
⊨
paircase
:
A1
+
A2
→
(
A1
⊸
B
)
⊸
(
A2
⊸
B
)
⊸
B
.
(* TODO: This probably requires there to be a rule that allows dropping arbitrary
resources from the postcondition. Check if there is such a rule. *)
Lemma
ltyped_case
Γ
1
Γ
2
Γ
3 e1
e2
e3
A1
A2
B
:
(
Γ
1
⊨
e1
:
A1
+
A2
⫤
Γ
2
)
-
∗
(
Γ
2
⊨
e2
:
A1
⊸
B
⫤
Γ
3
)
-
∗
(
Γ
2
⊨
e3
:
A2
⊸
B
⫤
Γ
3
)
-
∗
(
Γ
1
⊨
Case
e1
e2
e3
:
B
⫤
Γ
3
).
Proof
.
iIntros
(
vs
)
"!> HΓ /="
.
iApply
wp_value
.
iSplitL
;
last
by
iApply
env_ltyped_empty
.
rewrite
/
paircase
.
iIntros
"!>"
(
p
)
"Hp"
.
wp_pures
.
iIntros
(
f_left
)
"Hleft"
.
wp_pures
.
iIntros
(
f_right
)
"Hright"
.
wp_pures
.
iDestruct
"Hp"
as
"[Hp|Hp]"
.
-
iDestruct
"Hp"
as
(
w1
->)
"Hp"
.
wp_pures
.
wp_apply
(
wp_wand
with
"(Hleft [Hp //])"
).
iIntros
(
v
)
"HB"
.
iApply
"HB"
.
-
iDestruct
"Hp"
as
(
w2
->)
"Hp"
.
wp_pures
.
wp_apply
(
wp_wand
with
"(Hright [Hp //])"
).
iIntros
(
v
)
"HB"
.
iApply
"HB"
.
iIntros
"#H1 #H2 #H3"
(
vs
)
"!> HΓ1 /="
.
wp_bind
(
subst_map
vs
e1
).
iSpecialize
(
"H1"
with
"HΓ1"
).
iApply
(
wp_wand
with
"H1"
).
iIntros
(
s
)
"[Hs HΓ2]"
.
iDestruct
"Hs"
as
"[Hs|Hs]"
;
iDestruct
"Hs"
as
(
w
->)
"HA"
;
wp_case
.
-
wp_bind
(
subst_map
vs
e2
).
iApply
(
wp_wand
with
"(H2 HΓ2)"
).
iIntros
(
v
)
"[Hv HΓ3]"
.
iApply
(
wp_wand
with
"(Hv HA)"
).
iIntros
(
v'
)
"HB"
.
iFrame
"HΓ3 HB"
.
-
wp_bind
(
subst_map
vs
e3
).
iApply
(
wp_wand
with
"(H3 HΓ2)"
).
iIntros
(
v
)
"[Hv HΓ3]"
.
iApply
(
wp_wand
with
"(Hv HA)"
).
iIntros
(
v'
)
"HB"
.
iFrame
"HΓ3 HB"
.
Qed
.
(** Universal Properties *)
...
...
@@ -242,280 +241,194 @@ Section properties.
wp_apply
(
wp_wand
with
"(He [HΓ //])"
)
;
iIntros
(
w
)
"[HB $]"
.
by
iExists
M
.
Qed
.
Lemma
ltyped_unpack
{
k
}
Γ
1
Γ
2
Γ
3
x
e1
e2
(
C
:
lty
Σ
k
→
ltty
Σ
)
B
:
(
Γ
1
⊨
e1
:
lty_exist
C
⫤
Γ
2
)
-
∗
(
∀
Y
,
binder_insert
x
(
C
Y
)
Γ
2
⊨
e2
:
B
⫤
Γ
3
)
-
∗
Γ
1
⊨
(
let
:
x
:
=
e1
in
e2
)
:
B
⫤
binder_delete
x
Γ
3
.
Lemma
ltyped_unpack
{
k
}
Γ
1
Γ
2
Γ
3
(
x
:
string
)
e
(
C
:
lty
Σ
k
→
ltty
Σ
)
A
:
Γ
1
!!
x
=
Some
(
lty_exist
C
)
→
(
∀
X
,
binder_insert
x
(
C
X
)
Γ
1
⊨
e
:
A
⫤
Γ
2
)
-
∗
(
Γ
1
⊨
e
:
A
⫤
Γ
2
)
.
Proof
.
iIntros
"#He1 #He2 !>"
.
iIntros
(
vs
)
"HΓ1"
=>
/=.
wp_apply
(
wp_wand
with
"(He1 HΓ1)"
).
iIntros
(
v
)
"[HC HΓ2]"
.
iDestruct
"HC"
as
(
X
)
"HX"
.
wp_pures
.
iDestruct
(
env_ltyped_insert
_
_
x
with
"HX HΓ2"
)
as
"HΓ2"
.
iDestruct
(
"He2"
with
"HΓ2"
)
as
"He2'"
.
destruct
x
as
[|
x
]
;
rewrite
/=
-
?subst_map_insert
//.
wp_apply
(
wp_wand
with
"He2'"
).
iIntros
(
w
)
"[HA2 HΓ3]"
.
iFrame
.
iApply
env_ltyped_delete
=>
//.
iIntros
(
Hx
)
"#He"
.
iIntros
(
vs
)
"!> HΓ"
.
iDestruct
(
env_ltyped_lookup
with
"HΓ"
)
as
(
v
Hv
)
"[HB HΓ]"
;
first
done
.
iDestruct
(
"HB"
)
as
(
B
)
"HB"
.
iDestruct
(
env_ltyped_insert
_
_
x
with
"HB HΓ"
)
as
"HΓ"
.
rewrite
/
binder_insert
insert_delete
(
insert_id
_
_
_
Hv
).