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
T
Tutorial POPL20
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
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
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Arthur Azevedo de Amorim
Tutorial POPL20
Commits
c147e8d1
Commit
c147e8d1
authored
Jan 19, 2020
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Various tweaks.
parent
166449ec
Changes
12
Hide whitespace changes
Inline
Side-by-side
Showing
12 changed files
with
86 additions
and
90 deletions
+86
-90
theories/compatibility.v
theories/compatibility.v
+5
-5
theories/fundamental.v
theories/fundamental.v
+5
-3
theories/interp.v
theories/interp.v
+3
-3
theories/language.v
theories/language.v
+15
-14
theories/parametricity.v
theories/parametricity.v
+10
-10
theories/safety.v
theories/safety.v
+4
-4
theories/sem_operators.v
theories/sem_operators.v
+4
-4
theories/sem_type_formers.v
theories/sem_type_formers.v
+2
-2
theories/sem_typed.v
theories/sem_typed.v
+9
-9
theories/sem_types.v
theories/sem_types.v
+1
-1
theories/typed.v
theories/typed.v
+1
-1
theories/unsafe.v
theories/unsafe.v
+27
-34
No files found.
theories/compatibility.v
View file @
c147e8d1
...
...
@@ -24,11 +24,11 @@ From tutorial_popl20 Require Export sem_typed sem_operators.
*)
Section
compatibility
.
Context
`
{
heapG
Σ
}.
Context
`
{
!
heapG
Σ
}.
Implicit
Types
A
B
:
sem_ty
Σ
.
Implicit
Types
C
:
sem_ty
Σ
→
sem_ty
Σ
.
Lemma
Var_sem_typed
Γ
(
x
:
string
)
A
:
Γ
!!
x
=
Some
A
→
Γ
⊨
x
:
A
.
Lemma
Var_sem_typed
Γ
(
x
:
string
)
A
:
Γ
!!
x
=
Some
A
→
(
Γ
⊨
x
:
A
)%
I
.
Proof
.
iIntros
(
H
Γ
x
vs
)
"!# #HΓ /="
.
iDestruct
(
env_sem_typed_lookup
with
"HΓ"
)
as
(
v
->)
"HA"
;
first
done
.
...
...
@@ -211,11 +211,11 @@ Section compatibility.
wp_apply
wp_fork
;
last
done
.
by
iApply
(
wp_wand
with
"(H [//])"
).
Qed
.
Lemma
UnitV_sem_typed
:
⊨
ᵥ
#()
:
()
.
Lemma
UnitV_sem_typed
:
(
⊨
ᵥ
#()
:
())%
I
.
Proof
.
by
iPureIntro
.
Qed
.
Lemma
BoolV_sem_typed
(
b
:
bool
)
:
⊨
ᵥ
#
b
:
sem_ty_bool
.
Lemma
BoolV_sem_typed
(
b
:
bool
)
:
(
⊨
ᵥ
#
b
:
sem_ty_bool
)%
I
.
Proof
.
by
iExists
b
.
Qed
.
Lemma
IntV_sem_typed
(
n
:
Z
)
:
⊨
ᵥ
#
n
:
sem_ty_int
.
Lemma
IntV_sem_typed
(
n
:
Z
)
:
(
⊨
ᵥ
#
n
:
sem_ty_int
)%
I
.
Proof
.
by
iExists
n
.
Qed
.
Lemma
PairV_sem_typed
v1
v2
τ
1
τ
2
:
...
...
theories/fundamental.v
View file @
c147e8d1
...
...
@@ -14,7 +14,7 @@ From tutorial_popl20 Require Export typed compatibility interp.
a straightforward induction on the typing derivation. *)
Section
fundamental
.
Context
`
{
heapG
Σ
}.
Context
`
{
!
heapG
Σ
}.
Implicit
Types
Γ
:
gmap
string
ty
.
Implicit
Types
τ
:
ty
.
Implicit
Types
ρ
:
list
(
sem_ty
Σ
).
...
...
@@ -28,8 +28,10 @@ Section fundamental.
ty_bin_op
op
τ
1
τ
2
σ
→
SemTyBinOp
op
(
⟦
τ
1
⟧
ρ
)
(
⟦
τ
2
⟧
ρ
)
(
⟦
σ
⟧
ρ
).
Proof
.
destruct
1
;
simpl
;
apply
_
.
Qed
.
Fixpoint
fundamental
Γ
e
τ
ρ
(
Hty
:
Γ
⊢
ₜ
e
:
τ
)
:
interp_env
Γ
ρ
⊨
e
:
⟦
τ
⟧
ρ
with
fundamental_val
v
τ
ρ
(
Hty
:
⊢
ᵥ
v
:
τ
)
:
⊨
ᵥ
v
:
⟦
τ
⟧
ρ
.
Lemma
fundamental
Γ
e
τ
ρ
(
Hty
:
Γ
⊢
ₜ
e
:
τ
)
:
(
interp_env
Γ
ρ
⊨
e
:
⟦
τ
⟧
ρ
)%
I
with
fundamental_val
v
τ
ρ
(
Hty
:
⊢
ᵥ
v
:
τ
)
:
(
⊨
ᵥ
v
:
⟦
τ
⟧
ρ
)%
I
.
Proof
.
-
destruct
Hty
;
simpl
.
+
iApply
Var_sem_typed
.
by
apply
lookup_interp_env
.
...
...
theories/interp.v
View file @
c147e8d1
...
...
@@ -5,7 +5,7 @@ From tutorial_popl20 Require Export sem_typed sem_type_formers types.
This is done by a straightforward induction on the syntactic type. *)
Reserved
Notation
"⟦ τ ⟧"
.
Fixpoint
interp
`
{
heapG
Σ
}
(
τ
:
ty
)
(
ρ
:
list
(
sem_ty
Σ
))
:
sem_ty
Σ
:
=
Fixpoint
interp
`
{
!
heapG
Σ
}
(
τ
:
ty
)
(
ρ
:
list
(
sem_ty
Σ
))
:
sem_ty
Σ
:
=
match
τ
return
_
with
|
TVar
x
=>
default
()
(
ρ
!!
x
)
(* dummy in case [x ∉ ρ] *)
|
TUnit
=>
()
...
...
@@ -27,7 +27,7 @@ Instance: Params (@interp) 2 := {}.
from type variables (that appear freely in [Γ]) to their corresponding
semantic types, we define a semantic typing context, i.e., a mapping
from variables (strings) to semantic types. *)
Definition
interp_env
`
{
heapG
Σ
}
(
Γ
:
gmap
string
ty
)
Definition
interp_env
`
{
!
heapG
Σ
}
(
Γ
:
gmap
string
ty
)
(
ρ
:
list
(
sem_ty
Σ
))
:
gmap
string
(
sem_ty
Σ
)
:
=
flip
interp
ρ
<$>
Γ
.
Instance
:
Params
(@
interp_env
)
3
:
=
{}.
...
...
@@ -37,7 +37,7 @@ Instance: Params (@interp_env) 3 := {}.
variables have on the interpretation of syntactic types and typing
contexts. *)
Section
interp_properties
.
Context
`
{
heapG
Σ
}.
Context
`
{
!
heapG
Σ
}.
Implicit
Types
Γ
:
gmap
string
ty
.
Implicit
Types
τ
:
ty
.
Implicit
Types
ρ
:
list
(
sem_ty
Σ
).
...
...
theories/language.v
View file @
c147e8d1
...
...
@@ -7,11 +7,11 @@ From iris.heap_lang.lib Require Export assert.
that one wishes to reason about, so as to make it possible that the same logic
can be used for a wide variety of languages. For the purpose of this lecture
material, we consider the concurrent ML-style language *HeapLang*, the default
language shipped with the Iris Coq development. We use
[HeapLang]
instead of
language shipped with the Iris Coq development. We use
HeapLang
instead of
defining our own language since the Iris development has support for nice
syntax for HeapLang programs, contains a number of useful tactics to enable
reasoning about HeapLang programs, and contains a number of results about
[HeapLang]
's metatheory (e.g. related to substitution).
HeapLang
's metatheory (e.g. related to substitution).
While HeapLang itself is an untyped language, the purpose of this tutorial is
to define a type system for HeapLang and to use semantic typing via logical
...
...
@@ -109,7 +109,7 @@ i.e. substitution will not go into them. *)
(** Now that we have defined our first HeapLang program, let us write a
specification for it in separation logic: *)
Lemma
wp_swap
`
{
heapG
Σ
}
l1
l2
v1
v2
:
Lemma
wp_swap
`
{
!
heapG
Σ
}
l1
l2
v1
v2
:
l1
↦
v1
-
∗
l2
↦
v2
-
∗
WP
swap
#
l1
#
l2
{{
v
,
⌜
v
=
#()
⌝
∗
l1
↦
v2
∗
l2
↦
v1
}}.
...
...
@@ -121,7 +121,7 @@ This specification already points out a number of interesting features of
both separation logic and the Iris framework:
- First, a very technical one: each Iris lemma that involves HeapLang programs,
should have the parameter [`{heapG Σ}]. This has to do with Iris's generic
should have the parameter [`{
!
heapG Σ}]. This has to do with Iris's generic
infrastructure for handling ghost state. For now, this can be mostly ignored,
but more information can be found at:
https://gitlab.mpi-sws.org/iris/iris/blob/master/docs/proof_guide.md#resource-algebra-management
...
...
@@ -214,7 +214,7 @@ Definition swap_and_add : val := λ: "l1" "l2",
"l2"
<-
"x"
.
(** The specification is as follows: *)
Lemma
wp_swap_and_add
`
{
heapG
Σ
}
l1
l2
(
x1
x2
:
Z
)
:
Lemma
wp_swap_and_add
`
{
!
heapG
Σ
}
l1
l2
(
x1
x2
:
Z
)
:
l1
↦
#
x1
-
∗
l2
↦
#
x2
-
∗
WP
swap_and_add
#
l1
#
l2
{{
v
,
⌜
v
=
#()
⌝
∗
l1
↦
#(
x1
+
x2
)
∗
l2
↦
#
x1
}}.
...
...
@@ -241,7 +241,7 @@ Definition twice : val := λ: "f" "x",
only use them in the conclusions of a lemma, but als in the premises, and in
arbitrarily nested ways. This is crucial to reason about higher-order functions.
Let us see that in action for the [twice] function. *)
Lemma
wp_twice
`
{
heapG
Σ
}
(
Ψ
:
val
→
iProp
Σ
)
(
vf
vx
:
val
)
:
Lemma
wp_twice
`
{
!
heapG
Σ
}
(
Ψ
:
val
→
iProp
Σ
)
(
vf
vx
:
val
)
:
WP
vf
vx
{{
w
,
WP
vf
w
{{
Ψ
}}
}}
-
∗
WP
twice
vf
vx
{{
Ψ
}}.
...
...
@@ -284,7 +284,7 @@ Definition add_two : val := λ: "x",
(** While this function is rather convoluted, the specification is precisely
what you would expect---it adds [2]. *)
Lemma
wp_add_two
`
{
heapG
Σ
}
(
x
:
Z
)
:
Lemma
wp_add_two
`
{
!
heapG
Σ
}
(
x
:
Z
)
:
WP
add_two
#
x
{{
w
,
⌜
w
=
#(
2
+
x
)
⌝
}}%
I
.
(** Note that this weakest precondition does not have a premise (i.e. the
lemma does not involve a magic wand [-∗] at the top-level, as we have seen in
...
...
@@ -315,13 +315,14 @@ Qed.
(** ** Exercise (add_two_ref, moderate) *)
(** Instead of using [twice] to add [2] to an integer value, we now use it to
add [2] to the value of a reference to an integer. *)
add [2] to the value of a reference to an integer. That is, we use [twice]
with a function that reads the reference and adds [1] to it. *)
Definition
add_two_ref
:
val
:
=
λ
:
"l"
,
twice
(
λ
:
<>,
"l"
<-
#
1
+
!
"l"
)
#().
(** The specification is as expected (it follows the pattern we have seen in
e.g. [swap_and_add]---we make use of the points-to connective [l ↦ #x]. *)
Lemma
wp_add_two_ref
`
{
heapG
Σ
}
l
(
x
:
Z
)
:
Lemma
wp_add_two_ref
`
{
!
heapG
Σ
}
l
(
x
:
Z
)
:
l
↦
#
x
-
∗
WP
add_two_ref
#
l
{{
w
,
⌜
w
=
#()
⌝
∗
l
↦
#(
2
+
x
)
}}%
I
.
...
...
@@ -352,7 +353,7 @@ Definition twice_ref : val := λ: "lf" "lx",
(** The specification of [twice_ref] follows that of [twice], but it quantifies
both over locations [lf] and [lx], and the HeapLang function [vf] and value [vx]
that they contain, respectively. *)
Lemma
wp_twice_ref
`
{
heapG
Σ
}
(
Ψ
:
val
→
iProp
Σ
)
lf
lx
(
vf
vx
:
val
)
:
Lemma
wp_twice_ref
`
{
!
heapG
Σ
}
(
Ψ
:
val
→
iProp
Σ
)
lf
lx
(
vf
vx
:
val
)
:
lf
↦
vf
-
∗
lx
↦
vx
-
∗
WP
vf
vx
{{
w
,
WP
vf
w
{{
w'
,
lf
↦
vf
-
∗
lx
↦
w'
-
∗
Ψ
#()
}}
}}
-
∗
...
...
@@ -407,7 +408,7 @@ Definition add_two_fancy : val := λ: "x",
twice_ref
"lf"
"lx"
;;
!
"lx"
.
Lemma
wp_add_two_fancy
`
{
heapG
Σ
}
(
x
:
Z
)
:
Lemma
wp_add_two_fancy
`
{
!
heapG
Σ
}
(
x
:
Z
)
:
WP
add_two_fancy
#
x
{{
w
,
⌜
w
=
#(
2
+
x
)
⌝
}}%
I
.
(* REMOVE *)
Proof
.
rewrite
/
add_two_fancy
.
wp_pures
.
...
...
@@ -426,7 +427,7 @@ Qed.
Definition
unsafe_pure
:
val
:
=
λ
:
<>,
if
:
#
true
then
#
13
else
#
13
#
37
.
Lemma
wp_unsafe_pure
`
{
heapG
Σ
}
:
Lemma
wp_unsafe_pure
`
{
!
heapG
Σ
}
:
WP
unsafe_pure
#()
{{
v
,
⌜
v
=
#
13
⌝
}}%
I
.
Proof
.
rewrite
/
unsafe_pure
.
...
...
@@ -438,7 +439,7 @@ Qed.
Definition
unsafe_ref
:
val
:
=
λ
:
<>,
let
:
"l"
:
=
ref
#
0
in
"l"
<-
#
true
;;
!
"l"
.
Lemma
wp_unsafe_ref
`
{
heapG
Σ
}
:
Lemma
wp_unsafe_ref
`
{
!
heapG
Σ
}
:
WP
unsafe_ref
#()
{{
v
,
⌜
v
=
#
true
⌝
}}%
I
.
(* REMOVE *)
Proof
.
rewrite
/
unsafe_ref
.
wp_pures
.
...
...
@@ -476,7 +477,7 @@ Definition swap_poly : val := Λ: λ: "l1" "l2",
"l1"
<-
!
"l2"
;;
"l2"
<-
"x"
.
Lemma
wp_swap_poly
`
{
heapG
Σ
}
l1
l2
v1
v2
:
Lemma
wp_swap_poly
`
{
!
heapG
Σ
}
l1
l2
v1
v2
:
l1
↦
v1
-
∗
l2
↦
v2
-
∗
WP
swap_poly
<
_
>
#
l1
#
l2
{{
v
,
⌜
v
=
#()
⌝
∗
l1
↦
v2
∗
l2
↦
v1
}}.
...
...
theories/parametricity.v
View file @
c147e8d1
From
tutorial_popl20
Require
Export
safety
.
Section
parametricity
.
Context
`
{
heapG
Σ
}.
Context
`
{
!
heapG
Σ
}.
Lemma
identity_param
`
{!
heapPreG
Σ
}
e
(
v
:
val
)
σ
w
es
σ
'
:
(
∀
`
{
heapG
Σ
},
∅
⊨
e
:
∀
A
,
A
→
A
)
→
(
∀
`
{
!
heapG
Σ
},
(
∅
⊨
e
:
∀
A
,
A
→
A
)%
I
)
→
rtc
erased_step
([
e
<
_
>
v
]%
E
,
σ
)
(
of_val
w
::
es
,
σ
'
)
→
w
=
v
.
Proof
.
intros
He
.
...
...
@@ -21,7 +21,7 @@ Section parametricity.
Qed
.
Lemma
empty_type_param
`
{!
heapPreG
Σ
}
e
(
v
:
val
)
σ
w
es
σ
'
:
(
∀
`
{
heapG
Σ
},
∅
⊨
e
:
∀
A
,
A
)
→
(
∀
`
{
!
heapG
Σ
},
(
∅
⊨
e
:
∀
A
,
A
)%
I
)
→
rtc
erased_step
([
e
<
_
>]%
E
,
σ
)
(
of_val
w
::
es
,
σ
'
)
→
False
.
(* REMOVE *)
Proof
.
...
...
@@ -39,7 +39,7 @@ Section parametricity.
Qed
.
Lemma
boolean_param
`
{!
heapPreG
Σ
}
e
(
v1
v2
:
val
)
σ
w
es
σ
'
:
(
∀
`
{
heapG
Σ
},
∅
⊨
e
:
∀
A
,
A
→
A
→
A
)
→
(
∀
`
{
!
heapG
Σ
},
(
∅
⊨
e
:
∀
A
,
A
→
A
→
A
)%
I
)
→
rtc
erased_step
([
e
<
_
>
v1
v2
]%
E
,
σ
)
(
of_val
w
::
es
,
σ
'
)
→
w
=
v1
∨
w
=
v2
.
(* REMOVE *)
Proof
.
intros
He
.
...
...
@@ -60,7 +60,7 @@ Section parametricity.
Qed
.
Lemma
nat_param
`
{!
heapPreG
Σ
}
e
σ
w
es
σ
'
:
(
∀
`
{
heapG
Σ
},
∅
⊨
e
:
∀
A
,
(
A
→
A
)
→
A
→
A
)
→
(
∀
`
{
!
heapG
Σ
},
(
∅
⊨
e
:
∀
A
,
(
A
→
A
)
→
A
→
A
)%
I
)
→
rtc
erased_step
([
e
<
_
>
(
λ
:
"n"
,
"n"
+
#
1
)%
V
#
0
]%
E
,
σ
)
(
of_val
w
::
es
,
σ
'
)
→
∃
n
:
nat
,
w
=
#
n
.
(* REMOVE *)
Proof
.
...
...
@@ -86,11 +86,11 @@ Section parametricity.
Qed
.
Lemma
strong_nat_param
`
{!
heapPreG
Σ
}
e
σ
w
es
σ
'
(
vf
vz
:
val
)
φ
:
(
∀
`
{
heapG
Σ
},
∃
Φ
:
sem_ty
Σ
,
(
∅
⊨
e
:
∀
A
,
(
A
→
A
)
→
A
→
A
)
∧
(
∀
w
,
{{{
Φ
w
}}}
vf
w
{{{
w'
,
RET
w'
;
Φ
w'
}}})
∧
(
Φ
vz
)
∧
(
∀
w
,
Φ
w
-
∗
⌜φ
w
⌝
))
→
(
∀
`
{
!
heapG
Σ
},
∃
Φ
:
sem_ty
Σ
,
(
∅
⊨
e
:
∀
A
,
(
A
→
A
)
→
A
→
A
)
%
I
∧
(
∀
w
,
{{{
Φ
w
}}}
vf
w
{{{
w'
,
RET
w'
;
Φ
w'
}}})
%
I
∧
(
Φ
vz
)
%
I
∧
(
∀
w
,
Φ
w
-
∗
⌜φ
w
⌝
)
%
I
)
→
rtc
erased_step
([
e
<
_
>
vf
vz
]%
E
,
σ
)
(
of_val
w
::
es
,
σ
'
)
→
φ
w
.
(* REMOVE *)
Proof
.
intros
He
.
...
...
theories/safety.v
View file @
c147e8d1
...
...
@@ -19,8 +19,8 @@ From tutorial_popl20 Require Export fundamental.
v)]. The proposition [adequate NotStuck e σ (λ v σ, φ v)] means
that [e], starting in heap [σ] does not get stuck, and if [e]
reduces to a value [v], we have [φ v]. *)
Lemma
sem_gen_type_safety
`
{
heapPreG
Σ
}
e
σ
φ
:
(
∀
`
{
heapG
Σ
},
∃
A
:
sem_ty
Σ
,
(
∀
v
,
A
v
-
∗
⌜φ
v
⌝
)
∧
(
∅
⊨
e
:
A
)
)
→
Lemma
sem_gen_type_safety
`
{
!
heapPreG
Σ
}
e
σ
φ
:
(
∀
`
{
!
heapG
Σ
},
∃
A
:
sem_ty
Σ
,
(
∀
v
,
A
v
-
∗
⌜φ
v
⌝
)
∧
(
∅
⊨
e
:
A
)%
I
)
→
adequate
NotStuck
e
σ
(
λ
v
σ
,
φ
v
).
Proof
.
intros
Hty
.
apply
(
heap_adequacy
Σ
NotStuck
e
σ
)=>
//
?.
...
...
@@ -34,8 +34,8 @@ Qed.
(** This lemma states that semantically typed closed programs do not
get stuck. It is a simple consequence of the lemma
[sem_gen_type_safety] above. *)
Lemma
sem_type_safety
`
{
heapPreG
Σ
}
e
σ
es
σ
'
e'
:
(
∀
`
{
heapG
Σ
},
∃
A
,
∅
⊨
e
:
A
)
→
Lemma
sem_type_safety
`
{
!
heapPreG
Σ
}
e
σ
es
σ
'
e'
:
(
∀
`
{
!
heapG
Σ
},
∃
A
,
(
∅
⊨
e
:
A
)%
I
)
→
rtc
erased_step
([
e
],
σ
)
(
es
,
σ
'
)
→
e'
∈
es
→
is_Some
(
to_val
e'
)
∨
reducible
e'
σ
'
.
Proof
.
...
...
theories/sem_operators.v
View file @
c147e8d1
From
tutorial_popl20
Require
Export
sem_typed
.
(* Typing for operators *)
Class
SemTyUnboxed
`
{
heapG
Σ
}
(
A
:
sem_ty
Σ
)
:
=
Class
SemTyUnboxed
`
{
!
heapG
Σ
}
(
A
:
sem_ty
Σ
)
:
=
sem_ty_unboxed
v
:
A
v
-
∗
⌜
val_is_unboxed
v
⌝
.
Class
SemTyUnOp
`
{
heapG
Σ
}
(
op
:
un_op
)
(
A
B
:
sem_ty
Σ
)
:
=
Class
SemTyUnOp
`
{
!
heapG
Σ
}
(
op
:
un_op
)
(
A
B
:
sem_ty
Σ
)
:
=
sem_ty_un_op
v
:
A
v
-
∗
∃
w
,
⌜
un_op_eval
op
v
=
Some
w
⌝
∧
B
w
.
Class
SemTyBinOp
`
{
heapG
Σ
}
(
op
:
bin_op
)
(
A1
A2
B
:
sem_ty
Σ
)
:
=
Class
SemTyBinOp
`
{
!
heapG
Σ
}
(
op
:
bin_op
)
(
A1
A2
B
:
sem_ty
Σ
)
:
=
sem_ty_bin_op
v1
v2
:
A1
v1
-
∗
A2
v2
-
∗
∃
w
,
⌜
bin_op_eval
op
v1
v2
=
Some
w
⌝
∧
B
w
.
Section
sem_operators
.
Context
`
{
heapG
Σ
}.
Context
`
{
!
heapG
Σ
}.
Implicit
Types
A
B
:
sem_ty
Σ
.
(* Unboxed types *)
...
...
theories/sem_type_formers.v
View file @
c147e8d1
...
...
@@ -8,7 +8,7 @@ From tutorial_popl20 Require Export sem_types.
pairs where the first component belongs to [A] and the second
component to [B]. *)
Section
types
.
Context
`
{
heapG
Σ
}.
Context
`
{
!
heapG
Σ
}.
(** Let us start with the simplest types of our language: unit and Boolean.
The value interpretations of these types are as follows: *)
...
...
@@ -128,7 +128,7 @@ Instance: Params (@sem_ty_ref) 2 := {}.
(** We prove that all type formers are non-expansive and respect setoid
equality. This code is mostly boilerplate. *)
Section
types_properties
.
Context
`
{
heapG
Σ
}.
Context
`
{
!
heapG
Σ
}.
Global
Instance
sem_ty_prod_ne
:
NonExpansive2
(@
sem_ty_prod
Σ
).
Proof
.
solve_proper
.
Qed
.
...
...
theories/sem_typed.v
View file @
c147e8d1
...
...
@@ -20,31 +20,32 @@ From tutorial_popl20 Require Export sem_type_formers.
(** The semantic type for the typing context (environment). *)
Definition
env_sem_typed
`
{
heapG
Σ
}
(
Γ
:
gmap
string
(
sem_ty
Σ
))
Definition
env_sem_typed
`
{
!
heapG
Σ
}
(
Γ
:
gmap
string
(
sem_ty
Σ
))
(
vs
:
gmap
string
val
)
:
iProp
Σ
:
=
([
∗
map
]
i
↦
A
;
v
∈
Γ
;
vs
,
sem_ty_car
A
v
)%
I
.
Instance
:
Params
(@
env_sem_typed
)
2
:
=
{}.
(** The semantics typing judgment. *)
Definition
sem_typed
`
{
heapG
Σ
}
Definition
sem_typed
`
{
!
heapG
Σ
}
(
Γ
:
gmap
string
(
sem_ty
Σ
))
(
e
:
expr
)
(
A
:
sem_ty
Σ
)
:
iProp
Σ
:
=
tc_opaque
(
□
∀
vs
,
env_sem_typed
Γ
vs
-
∗
WP
subst_map
vs
e
{{
A
}})%
I
.
tc_opaque
(
□
∀
vs
,
env_sem_typed
Γ
vs
-
∗
WP
subst_map
vs
e
{{
A
}})%
I
.
Instance
:
Params
(@
sem_typed
)
2
:
=
{}.
Notation
"Γ ⊨ e : A"
:
=
(
sem_typed
Γ
e
A
)
(
at
level
74
,
e
,
A
at
next
level
).
(
at
level
74
,
e
,
A
at
next
level
)
:
bi_scope
.
Definition
sem_val_typed
`
{
heapG
Σ
}
(
v
:
val
)
(
A
:
sem_ty
Σ
)
:
iProp
Σ
:
=
Definition
sem_val_typed
`
{
!
heapG
Σ
}
(
v
:
val
)
(
A
:
sem_ty
Σ
)
:
iProp
Σ
:
=
tc_opaque
(
A
v
).
Instance
:
Params
(@
sem_val_typed
)
3
:
=
{}.
Notation
"⊨ᵥ v : A"
:
=
(
sem_val_typed
v
A
)
(
at
level
20
,
v
,
A
at
next
level
).
(
at
level
20
,
v
,
A
at
next
level
)
:
bi_scope
.
Arguments
sem_val_typed
:
simpl
never
.
(** A few useful lemmas about the semantic typing judgment. The first
few lemmas involving [Proper]ness are boilerplate required for supporting setoid
rewriting. *)
Section
sem_typed
.
Context
`
{
heapG
Σ
}.
Context
`
{
!
heapG
Σ
}.
Implicit
Types
A
B
:
sem_ty
Σ
.
Implicit
Types
C
:
sem_ty
Σ
→
sem_ty
Σ
.
...
...
@@ -69,8 +70,7 @@ Section sem_typed.
Global
Instance
sem_typed_persistent
Γ
e
A
:
Persistent
(
Γ
⊨
e
:
A
).
Proof
.
rewrite
/
sem_typed
/=.
apply
_
.
Qed
.
Global
Instance
sem_val_typed_ne
n
v
:
Proper
(
dist
n
==>
dist
n
)
(@
sem_val_typed
Σ
_
v
).
Global
Instance
sem_val_typed_ne
v
:
NonExpansive
(@
sem_val_typed
Σ
_
v
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
sem_val_typed_proper
v
:
Proper
((
≡
)
==>
(
≡
))
(@
sem_val_typed
Σ
_
v
).
...
...
theories/sem_types.v
View file @
c147e8d1
...
...
@@ -47,7 +47,7 @@ Existing Instance sem_ty_persistent.
(* The COFE structure on semantic types *)
Section
sem_ty_cofe
.
Context
`
{
Σ
:
gFunctors
}.
Context
{
Σ
:
gFunctors
}.
Instance
sem_ty_equiv
:
Equiv
(
sem_ty
Σ
)
:
=
λ
A
B
,
∀
w
,
A
w
≡
B
w
.
Instance
sem_ty_dist
:
Dist
(
sem_ty
Σ
)
:
=
λ
n
A
B
,
∀
w
,
A
w
≡
{
n
}
≡
B
w
.
...
...
theories/typed.v
View file @
c147e8d1
...
...
@@ -38,7 +38,7 @@ Inductive typed : gmap string ty → expr → ty → Prop :=
Γ
⊢
ₜ
Var
x
:
τ
(** Values *)
|
Val_typed
Γ
v
τ
:
val_typed
v
τ
→
⊢
ᵥ
v
:
τ
→
Γ
⊢
ₜ
v
:
τ
(** Products and sums *)
|
Pair_typed
Γ
e1
e2
τ
1
τ
2
:
...
...
theories/unsafe.v
View file @
c147e8d1
...
...
@@ -2,37 +2,34 @@ From tutorial_popl20 Require Export sem_typed.
From
tutorial_popl20
Require
Import
symbol_ghost
two_state_ghost
.
Section
unsafe
.
Context
`
{
heapG
Σ
}.
Context
`
{
!
heapG
Σ
}.
(** * Exercise (easy) *)
(** Recall the following function we defined in the file [language.v]:
<<
Definition unsafe_pure : val := λ: <>,
if: #true then #13 else #13 #37.
Lemma
sem_typed_unsafe_pure
:
∅
⊨
unsafe_pure
:
(()
→
sem_ty_int
).
>>
*)
Lemma
sem_typed_unsafe_pure
:
(
∅
⊨
unsafe_pure
:
(()
→
sem_ty_int
))%
I
.
Proof
.
iIntros
(
vs
)
"!# HΓ"
;
simpl
.
iApply
wp_value
.
iIntros
"!#"
(?
->).
wp_lam
.
wp_if
.
iIntros
(
vs
)
"!# HΓ /="
.
iApply
wp_value
.
iIntros
"!#"
(?
->).
wp_lam
.
wp_if
.
rewrite
/
sem_ty_car
/=.
by
iExists
13
.
Qed
.
(** * Exercise (easy) *)
(** Recall the following function we defined in the file [language.v]:
<<
Definition unsafe_ref : val := λ: <>,
let: "l" := ref #0 in "l" <- #true;; !"l".
Lemma
sem_typed_unsafe_ref
:
∅
⊨
unsafe_ref
:
(()
→
sem_ty_bool
)
.
>> *)
Lemma
sem_typed_unsafe_ref
:
(
∅
⊨
unsafe_ref
:
(()
→
sem_ty_bool
))%
I
.
Proof
.
iIntros
(
vs
)
"!# HΓ"
;
simpl
.
iApply
wp_value
.
iIntros
"!#"
(?
->).
wp_lam
.
iIntros
(
vs
)
"!# HΓ /="
.
iApply
wp_value
.
iIntros
"!#"
(?
->).
wp_lam
.
wp_alloc
l
as
"Hl"
.
wp_let
.
wp_store
.
wp_load
.
wp_store
.
wp_load
.
rewrite
/
sem_ty_car
/=.
by
iExists
true
.
Qed
.
...
...
@@ -44,14 +41,11 @@ Section unsafe.
(
λ
:
<>,
assert
:
!
"l"
≠
#
0
)).
Lemma
sem_typed_unsafe_ref_ne_0
:
∅
⊨
unsafe_ref_ne_0
:
(()
→
(
sem_ty_int
→
())
*
(()
→
()))
.
(
∅
⊨
unsafe_ref_ne_0
:
(()
→
(
sem_ty_int
→
())
*
(()
→
())))%
I
.
Proof
.
iIntros
(
vs
)
"!# HΓ"
;
simpl
.
iApply
wp_value
.
iIntros
(
vs
)
"!# HΓ /="
.
iApply
wp_value
.
iIntros
"!#"
(?
->).
wp_lam
.
wp_alloc
l
as
"Hl"
.
wp_let
.
wp_lam
.
wp_alloc
l
as
"Hl"
.
wp_let
.
pose
(
I
:
=
(
∃
n
:
Z
,
⌜
#
n
≠
#
0
⌝
∗
l
↦
#
n
)%
I
).
iMod
(
inv_alloc
(
nroot
.@
"inv"
)
_
I
with
"[Hl]"
)%
I
as
"#Hinv"
.
{
by
iNext
;
iExists
1
;
iFrame
.
}
...
...
@@ -92,13 +86,11 @@ Section unsafe.
Definition
unsafe_ref_reuse
:
val
:
=
λ
:
<>,
let
:
"l"
:
=
ref
#
0
in
λ
:
<>,
"l"
<-
#
true
;;
!
"l"
.
Lemma
sem_typed_unsafe_ref_reuse
`
{
two_stateG
Σ
}
:
∅
⊨
unsafe_ref_reuse
:
(()
→
(()
→
sem_ty_bool
))
.
Lemma
sem_typed_unsafe_ref_reuse
`
{
!
two_stateG
Σ
}
:
(
∅
⊨
unsafe_ref_reuse
:
(()
→
(()
→
sem_ty_bool
)))%
I
.
Proof
.
iIntros
(
vs
)
"!# HΓ"
;
simpl
.
iApply
wp_value
.
iIntros
"!#"
(?
->).
wp_lam
.
iIntros
(
vs
)
"!# HΓ /="
.
iApply
wp_value
.
iIntros
"!#"
(?
->).
wp_lam
.
wp_alloc
l
as
"Hl"
.
iMod
two_state_init
as
(
γ
)
"Ho"
.
pose
(
I
:
=
(
∃
b
,
two_state_auth
γ
b
∗
l
↦
(
if
b
then
#
true
else
#
0
))%
I
).
...
...
@@ -128,13 +120,14 @@ Section unsafe.
Definition
symbol_adt_inc
:
val
:
=
λ
:
"x"
<>,
FAA
"x"
#
1
.
Definition
symbol_adt_check
:
val
:
=
λ
:
"x"
"y"
,
assert
:
"y"
<
!
"x"
.
Definition
symbol_adt
:
val
:
=
λ
:
<>,
let
:
"x"
:
=
Alloc
#
0
in
pack
:
(
symbol_adt_inc
"x"
,
symbol_adt_check
"x"
).
let
:
"x"
:
=
Alloc
#
0
in
pack
:
(
symbol_adt_inc
"x"
,
symbol_adt_check
"x"
).
Definition
symbol_adt_ty
`
{
heapG
Σ
}
:
sem_ty
Σ
:
=
Definition
symbol_adt_ty
:
sem_ty
Σ
:
=
(()
→
∃
A
,
(()
→
A
)
*
(
A
→
())).
Section
sem_typed_symbol_adt
.
Context
`
{
symbolG
Σ
}.
Context
`
{
!
symbolG
Σ
}.
Definition
symbol_adtN
:
=
nroot
.@
"symbol_adt"
.
...
...
@@ -144,7 +137,7 @@ Section unsafe.
Definition
sem_ty_symbol
(
γ
:
gname
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
n
:
nat
,
⌜
w
=
#
n
⌝
∧
symbol
γ
n
)%
I
.
Lemma
sem_typed_symbol_adt
Γ
:
Γ
⊨
symbol_adt
:
symbol_adt_ty
.
Lemma
sem_typed_symbol_adt
Γ
:
(
Γ
⊨
symbol_adt
:
symbol_adt_ty
)%
I
.
Proof
.
iIntros
(
vs
)
"!# _ /="
.
iApply
wp_value
.
iIntros
"!#"
(
v
->).
wp_lam
.
wp_alloc
l
as
"Hl"
;
wp_pures
.
...
...
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