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
e5303d75
Commit
e5303d75
authored
Jan 20, 2020
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Make make work.
parent
fb64a614
Changes
9
Hide whitespace changes
Inline
Side-by-side
Showing
9 changed files
with
240 additions
and
259 deletions
+240
-259
exercises/compatibility.v
exercises/compatibility.v
+15
-23
exercises/language.v
exercises/language.v
+4
-4
exercises/parametricity.v
exercises/parametricity.v
+4
-4
exercises/polymorphism.v
exercises/polymorphism.v
+1
-1
exercises/sem_type_formers.v
exercises/sem_type_formers.v
+101
-105
exercises/typed.v
exercises/typed.v
+9
-9
mk-exercises.sh
mk-exercises.sh
+1
-1
solutions/compatibility.v
solutions/compatibility.v
+4
-4
solutions/sem_type_formers.v
solutions/sem_type_formers.v
+101
-108
No files found.
exercises/compatibility.v
View file @
e5303d75
...
...
@@ -58,29 +58,21 @@ Section compatibility.
iDestruct
1
as
(
w1
w2
->)
"[??]"
.
by
wp_pures
.
Qed
.
Lemma
Snd_sem_typed
Γ
e
A1
A2
:
Γ
⊨
e
:
A1
*
A2
-
∗
Γ
⊨
Snd
e
:
A2
.
Proof
.
iIntros
"#H"
(
vs
)
"!# #HΓ /="
.
wp_apply
(
wp_wand
with
"(H [//])"
)
;
iIntros
(
w
).
iDestruct
1
as
(
w1
w2
->)
"[??]"
.
by
wp_pures
.
Qed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitted
.
Lemma
InjL_sem_typed
Γ
e
A1
A2
:
Γ
⊨
e
:
A1
-
∗
Γ
⊨
InjL
e
:
A1
+
A2
.
Proof
.
(* FILL IN YOUR PROOF *)
Qed
.
(* REMOVE *)
Lemma
InjR_sem_typed
Γ
e
A1
A2
:
Γ
⊨
e
:
A2
-
∗
Γ
⊨
InjR
e
:
A1
+
A2
.
Proof
.
iIntros
"#H"
(
vs
)
"!# #HΓ /="
.
wp_apply
(
wp_wand
with
"(H [//])"
)
;
iIntros
(
w
)
"#HA"
.
wp_pures
.
iRight
.
iExists
w
.
auto
.
Qed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitted
.
Lemma
InjR_sem_typed
Γ
e
A1
A2
:
Γ
⊨
e
:
A2
-
∗
Γ
⊨
InjR
e
:
A1
+
A2
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitted
.
Lemma
Case_sem_typed
Γ
e
e1
e2
A1
A2
B
:
Γ
⊨
e
:
A1
+
A2
-
∗
Γ
⊨
e1
:
(
A1
→
B
)
-
∗
Γ
⊨
e2
:
(
A2
→
B
)
-
∗
Γ
⊨
Case
e
e1
e2
:
B
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
(** * Functions *)
Lemma
Rec_sem_typed
Γ
f
x
e
A1
A2
:
binder_insert
f
(
A1
→
A2
)%
sem_ty
(
binder_insert
x
A1
Γ
)
⊨
e
:
A2
-
∗
Γ
⊨
(
rec
:
f
x
.
(* FILL IN HERE *)
Admitted
.
Γ
⊨
(
rec
:
f
x
:
=
e
)
:
(
A1
→
A2
)
.
Proof
.
iIntros
"#H"
(
vs
)
"!# #HΓ /="
.
wp_pures
.
iL
ö
b
as
"IH"
.
iIntros
"!#"
(
v
)
"#HA1"
.
wp_pures
.
set
(
r
:
=
RecV
f
x
_
).
...
...
@@ -109,11 +101,11 @@ Section compatibility.
Qed
.
Lemma
Pack_sem_typed
Γ
e
C
A
:
Γ
⊨
e
:
C
A
-
∗
Γ
⊨
(
pack
:
e
)
:
∃
A
,
C
A
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
Lemma
Unpack_sem_typed
Γ
x
e1
e2
C
B
:
(
Γ
⊨
e1
:
∃
A
,
C
A
)
-
∗
(
∀
A
,
binder_insert
x
(
C
A
)
Γ
⊨
e2
:
B
)
-
∗
Γ
⊨
(
unpack
:
x
:
=
e1
in
e2
)
:
B
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
(** ** Heap operations *)
Lemma
Alloc_sem_typed
Γ
e
A
:
Γ
⊨
e
:
A
-
∗
Γ
⊨
ref
e
:
ref
A
.
...
...
@@ -134,15 +126,15 @@ Section compatibility.
Qed
.
Lemma
Store_sem_typed
Γ
e1
e2
A
:
Γ
⊨
e1
:
ref
A
-
∗
Γ
⊨
e2
:
A
-
∗
Γ
⊨
(
e1
<-
e2
)
:
().
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
Lemma
FAA_sem_typed
Γ
e1
e2
:
Γ
⊨
e1
:
ref
sem_ty_int
-
∗
Γ
⊨
e2
:
sem_ty_int
-
∗
Γ
⊨
FAA
e1
e2
:
sem_ty_int
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
Lemma
CmpXchg_sem_typed
Γ
A
e1
e2
e3
:
SemTyUnboxed
A
→
Γ
⊨
e1
:
ref
A
-
∗
Γ
⊨
e2
:
A
-
∗
Γ
⊨
e3
:
A
-
∗
Γ
⊨
CmpXchg
e1
e2
e3
:
A
*
sem_ty_bool
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
(** ** Operators *)
Lemma
UnOp_sem_typed
Γ
e
op
A
B
:
...
...
@@ -154,16 +146,16 @@ Section compatibility.
Qed
.
Lemma
BinOp_sem_typed
Γ
e1
e2
op
A1
A2
B
:
SemTyBinOp
op
A1
A2
B
→
Γ
⊨
e1
:
A1
-
∗
Γ
⊨
e2
:
A2
-
∗
Γ
⊨
BinOp
op
e1
e2
:
B
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
Lemma
If_sem_typed
Γ
e
e1
e2
B
:
Γ
⊨
e
:
sem_ty_bool
-
∗
Γ
⊨
e1
:
B
-
∗
Γ
⊨
e2
:
B
-
∗
Γ
⊨
(
if
:
e
then
e1
else
e2
)
:
B
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
(** ** Fork *)
Lemma
Fork_sem_typed
Γ
e
:
Γ
⊨
e
:
()
-
∗
Γ
⊨
Fork
e
:
().
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
(** * Compatibility rules for value typing *)
(** ** Base types *)
...
...
@@ -172,7 +164,7 @@ Section compatibility.
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
)%
I
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
(** ** Products and sums *)
Lemma
PairV_sem_typed
v1
v2
τ
1
τ
2
:
...
...
exercises/language.v
View file @
e5303d75
...
...
@@ -233,7 +233,7 @@ You should prove this lemma.
Hint: [wp_pures] also executes the [+] operator. Carefully check how it affects
the embedded [#] and convince yourself why that makes sense. *)
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
(** ** Reasoning about higher-order functions *)
(** For the next example, let us consider the higher-order function [twice].
...
...
@@ -336,7 +336,7 @@ Lemma wp_add_two_ref `{!heapG Σ} l (x : Z) :
about addition on [Z] (or the [replace] or [rewrite (_ : x = y)] tactic with
[lia]) to turn [2 + x] into [1 + (1 + x)]. Tactics like [replace] and [rewrite]
work operate both on the MoSeL proof goal and the MoSeL proof context. *)
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
(** ** Reasoning about higher-order state *)
(** To see how Iris can be used to reason about higher-order state---that is,
...
...
@@ -407,7 +407,7 @@ Definition add_two_fancy : val := λ: "x",
Lemma
wp_add_two_fancy
`
{!
heapG
Σ
}
(
x
:
Z
)
:
WP
add_two_fancy
#
x
{{
w
,
⌜
w
=
#(
2
+
x
)
⌝
}}%
I
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
(** * Reasoning about "unsafe" programs *)
(** Since HeapLang is an untyped language, we can write down arbitrary
...
...
@@ -438,4 +438,4 @@ Definition unsafe_ref : val := λ: <>,
Lemma
wp_unsafe_ref
`
{!
heapG
Σ
}
:
WP
unsafe_ref
#()
{{
v
,
⌜
v
=
#
true
⌝
}}%
I
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
exercises/parametricity.v
View file @
e5303d75
...
...
@@ -27,20 +27,20 @@ Section parametricity.
(
∀
`
{!
heapG
Σ
},
(
∅
⊨
e
:
∀
A
,
A
)%
I
)
→
rtc
erased_step
([
e
<
_
>]%
E
,
σ
)
(
of_val
w
::
es
,
σ
'
)
→
False
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
(** * Exercise (boolean_param, moderate) *)
Lemma
boolean_param
`
{!
heapPreG
Σ
}
e
(
v1
v2
:
val
)
σ
w
es
σ
'
:
(
∀
`
{!
heapG
Σ
},
(
∅
⊨
e
:
∀
A
,
A
→
A
→
A
)%
I
)
→
rtc
erased_step
([
e
<
_
>
v1
v2
]%
E
,
σ
)
(
of_val
w
::
es
,
σ
'
)
→
w
=
v1
∨
w
=
v2
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
(** * Exercise (nat_param, hard) *)
Lemma
nat_param
`
{!
heapPreG
Σ
}
e
σ
w
es
σ
'
:
(
∀
`
{!
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
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
(** * Exercise (strong_nat_param, hard) *)
Lemma
strong_nat_param
`
{!
heapPreG
Σ
}
e
σ
w
es
σ
'
(
vf
vz
:
val
)
φ
:
...
...
@@ -50,5 +50,5 @@ Section parametricity.
(
Φ
vz
)%
I
∧
(
∀
w
,
Φ
w
-
∗
⌜φ
w
⌝
)%
I
)
→
rtc
erased_step
([
e
<
_
>
vf
vz
]%
E
,
σ
)
(
of_val
w
::
es
,
σ
'
)
→
φ
w
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
End
parametricity
.
exercises/polymorphism.v
View file @
e5303d75
...
...
@@ -44,4 +44,4 @@ Lemma wp_swap_poly `{!heapG Σ} l1 l2 v1 v2 :
l1
↦
v1
-
∗
l2
↦
v2
-
∗
WP
swap_poly
<
_
>
#
l1
#
l2
{{
v
,
⌜
v
=
#()
⌝
∗
l1
↦
v2
∗
l2
↦
v1
}}.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
exercises/sem_type_formers.v
View file @
e5303d75
...
...
@@ -7,109 +7,105 @@ formers, which given two semantic types [A] and [B], gives the semantic type of
the product [A * B], i.e., values that are pairs where the first component
belongs to [A] and the second component to [B]. *)
Section
types
.
Context
`
{!
heapG
Σ
}.
(** * Base types *)
(** Let us start with the simplest types of our language: unit and Boolean.
The corresponding semantic types are defined as follows: *)
Definition
sem_ty_unit
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
⌜
w
=
#()
⌝
)%
I
.
Definition
sem_ty_bool
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
b
:
bool
,
⌜
w
=
#
b
⌝
)%
I
.
(** These interpretations are exactly what you would expect: the only value
of the unit type is the unit value [()], the values of the Boolean type are
the elements of the Coq type [bool] (i.e. [true] and [false]). *)
(** ** Exercise (sem_ty_int, easy) *)
(** Define the semantic version of the type of integers. *)
Definition
sem_ty_int
:
sem_ty
Σ
.
(* FILL IN HERE *)
Admitted
.
(** * Products and sums *)
(** The semantic type former for products is as follows: *)
Definition
sem_ty_prod
(
A1
A2
:
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
w1
w2
,
⌜
w
=
(
w1
,
w2
)%
V
⌝
∧
A1
w1
∧
A2
w2
)%
I
.
(** Values of the product type over [A1] and [A2] should be tuples [(w1, w2)],
where [w1] and [w2] should values in the semantic type [A1] and [A2],
respectively. *)
(** ** Exercise (sem_ty_sum, moderate) *)
(** Define the semantic type former for sums. *)
Definition
sem_ty_sum
(
A1
A2
:
sem_ty
Σ
)
:
sem_ty
Σ
.
(* FILL IN HERE *)
Admitted
.
(** * Functions *)
(** The semantic type former for functions is as follows: *)
Definition
sem_ty_arr
(
A1
A2
:
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
□
∀
v
,
A1
v
-
∗
WP
App
w
v
{{
A2
}})%
I
.
(** This definition is very close to the usual way of defining the type
former for the function type [A1 → A2] in traditional logical relations: it
expresses that arguments of semantic type [A1] are mapped to results of
semantic type [A2]. The definition makes two of two features of Iris:
- The weakest precondition [WP e {{ Φ }}].
- The persistence modality [□]. Recall that semantic types are persistent Iris
predicates. However, even if both [P] and [Q] are persistent propositions,
the magic wand [P -∗ Q] is not necessarily persistent. Hence, we use the [□
modality to make the magic wand persistent.
*)
(** * Polymorphism and existentials *)
Definition
sem_ty_forall
(
C
:
sem_ty
Σ
→
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
□
∀
A
:
sem_ty
Σ
,
WP
w
#()
{{
w
,
C
A
w
}})%
I
.
Definition
sem_ty_exist
(
C
:
sem_ty
Σ
→
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
A
:
sem_ty
Σ
,
C
A
w
)%
I
.
(** The interpretations of these types are fairly straightforward.
Given a higher-order type former [C] that maps semantic types to
semantic types, we define the universal type [sem_ty_forall A]
using the universal quantification in Iris. That is, a value [w]
is considered a polymorphic value if for any semantic type [A],
when [w] is specialized to the type [A] (written as [w #()] as
(semantic) types never appear in terms in our untyped syntax)
the _resulting expression_ is an expression in the semantics of
the type [C A] (defined using WP).
Similarly, given a higher-order type former [C] that maps
semantic types to semantic types, we define the existential type
[sem_ty_exist A] using the existential quantification in Iris.
Notice how the impredicative nature of Iris propositions and
predicates allows us to quantify over Iris predicates to define
an Iris predicate. This is crucial for giving semantics to
parametric polymorphism, i.e., universal and existential types.
Remark: notice that for technical reasons (related to the value
restriction problem in ML-like languages) universally quantified
expressions are not evaluated until they are applied to a
specific type. *)
(** * References *)
Definition
tyN
:
=
nroot
.@
"ty"
.
Definition
sem_ty_ref
(
A
:
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
l
:
loc
,
⌜
w
=
#
l
⌝
∧
inv
(
tyN
.@
l
)
(
∃
v
,
l
↦
v
∗
A
v
))%
I
.
(** Intuitively, values of the reference type [sem_ty_ref A] should
be locations [l] that hold a value [w] in the semantic type [A] at
all times. In order to express this intuition in a formal way, we
make use of two features of Iris:
- The points-to connective l ↦ v (from vanilla separation logic)
provides exclusive ownership of the location l with value
v. The points-to connective is an ephemeral proposition, and
necessarily not a persistent proposition.
- The invariant assertion [inv N P] expresses that a (typically
ephemeral) proposition [P] holds at all times -- i.e., [P] is
invariant. The invariant assertion is persistent.
*)
(** Remark: Iris is also capable giving semantics to recursive
types. However, for the sake of simplicity we did not consider
recursive types for this tutorial. In particular, to give the
semantics of recursive types one needs to use Iris's guarded
fixpoints, which require some additional bookkeeping related to
contractiveness. *)
End
types
.
(** * Base types *)
(** Let us start with the simplest types of our language: unit, Boolean, and
integers. The corresponding semantic types are defined as follows: *)
Definition
sem_ty_unit
{
Σ
}
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
⌜
w
=
#()
⌝
)%
I
.
Definition
sem_ty_bool
{
Σ
}
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
b
:
bool
,
⌜
w
=
#
b
⌝
)%
I
.
Definition
sem_ty_int
{
Σ
}
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
n
:
Z
,
⌜
w
=
#
n
⌝
)%
I
.
(** These interpretations are exactly what you would expect: the only value
of the unit type is the unit value [()], the values of the Boolean type are
the elements of the Coq type [bool] (i.e. [true] and [false]), and the values
of the integer type are the integer literals. *)
(** * Products and sums *)
(** The semantic type former for products is as follows: *)
Definition
sem_ty_prod
{
Σ
}
(
A1
A2
:
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
w1
w2
,
⌜
w
=
(
w1
,
w2
)%
V
⌝
∧
A1
w1
∧
A2
w2
)%
I
.
(** Values of the product type over [A1] and [A2] should be tuples [(w1, w2)],
where [w1] and [w2] should values in the semantic type [A1] and [A2],
respectively. *)
(** The type former for sums is similar. *)
Definition
sem_ty_sum
{
Σ
}
(
A1
A2
:
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
(
∃
w1
,
⌜
w
=
InjLV
w1
⌝
∧
A1
w1
)
∨
(
∃
w2
,
⌜
w
=
InjRV
w2
⌝
∧
A2
w2
))%
I
.
(** * Functions *)
(** The semantic type former for functions is as follows: *)
Definition
sem_ty_arr
`
{!
heapG
Σ
}
(
A1
A2
:
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
□
∀
v
,
A1
v
-
∗
WP
App
w
v
{{
A2
}})%
I
.
(** This definition is very close to the usual way of defining the type
former for the function type [A1 → A2] in traditional logical relations: it
expresses that arguments of semantic type [A1] are mapped to results of
semantic type [A2]. The definition makes two of two features of Iris:
- The weakest precondition [WP e {{ Φ }}].
- The persistence modality [□]. Recall that semantic types are persistent Iris
predicates. However, even if both [P] and [Q] are persistent propositions,
the magic wand [P -∗ Q] is not necessarily persistent. Hence, we use the [□
modality to make the magic wand persistent.
*)
(** * Polymorphism and existentials *)
Definition
sem_ty_forall
`
{!
heapG
Σ
}
(
C
:
sem_ty
Σ
→
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
□
∀
A
:
sem_ty
Σ
,
WP
w
#()
{{
w
,
C
A
w
}})%
I
.
Definition
sem_ty_exist
{
Σ
}
(
C
:
sem_ty
Σ
→
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
A
:
sem_ty
Σ
,
C
A
w
)%
I
.
(** The interpretations of these types are fairly straightforward.
Given a higher-order type former [C] that maps semantic types to
semantic types, we define the universal type [sem_ty_forall A]
using the universal quantification in Iris. That is, a value [w]
is considered a polymorphic value if for any semantic type [A],
when [w] is specialized to the type [A] (written as [w #()] as
(semantic) types never appear in terms in our untyped syntax)
the _resulting expression_ is an expression in the semantics of
the type [C A] (defined using WP).
Similarly, given a higher-order type former [C] that maps
semantic types to semantic types, we define the existential type
[sem_ty_exist A] using the existential quantification in Iris.
Notice how the impredicative nature of Iris propositions and
predicates allows us to quantify over Iris predicates to define
an Iris predicate. This is crucial for giving semantics to
parametric polymorphism, i.e., universal and existential types.
Remark: notice that for technical reasons (related to the value
restriction problem in ML-like languages) universally quantified
expressions are not evaluated until they are applied to a
specific type. *)
(** * References *)
Definition
tyN
:
=
nroot
.@
"ty"
.
Definition
sem_ty_ref
`
{!
heapG
Σ
}
(
A
:
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
l
:
loc
,
⌜
w
=
#
l
⌝
∧
inv
(
tyN
.@
l
)
(
∃
v
,
l
↦
v
∗
A
v
))%
I
.
(** Intuitively, values of the reference type [sem_ty_ref A] should
be locations [l] that hold a value [w] in the semantic type [A] at
all times. In order to express this intuition in a formal way, we
make use of two features of Iris:
- The points-to connective l ↦ v (from vanilla separation logic)
provides exclusive ownership of the location l with value
v. The points-to connective is an ephemeral proposition, and
necessarily not a persistent proposition.
- The invariant assertion [inv N P] expresses that a (typically
ephemeral) proposition [P] holds at all times -- i.e., [P] is
invariant. The invariant assertion is persistent.
*)
(** Remark: Iris is also capable giving semantics to recursive
types. However, for the sake of simplicity we did not consider
recursive types for this tutorial. In particular, to give the
semantics of recursive types one needs to use Iris's guarded
fixpoints, which require some additional bookkeeping related to
contractiveness. *)
(** We introduce nicely looking notations for our semantic types. This allows
us to write lemmas, for example, the compatibility lemmas, in a readable way. *)
...
...
@@ -126,10 +122,10 @@ Notation "'ref' A" := (sem_ty_ref A) : sem_ty_scope.
(** A [Params t n] instance tells Coq's setoid rewriting mechanism *not* to
rewrite in the first [n] arguments of [t]. These instances tend to make the
setoid rewriting mechanism a lot faster. This code is mostly boilerplate. *)
Instance
:
Params
(@
sem_ty_arr
)
1
:
=
{}.
Instance
:
Params
(@
sem_ty_prod
)
1
:
=
{}.
Instance
:
Params
(@
sem_ty_sum
)
1
:
=
{}.
Instance
:
Params
(@
sem_ty_forall
)
1
:
=
{}.
Instance
:
Params
(@
sem_ty_arr
)
1
:
=
{}.
Instance
:
Params
(@
sem_ty_forall
)
2
:
=
{}.
Instance
:
Params
(@
sem_ty_exist
)
1
:
=
{}.
Instance
:
Params
(@
sem_ty_ref
)
2
:
=
{}.
...
...
exercises/typed.v
View file @
e5303d75
...
...
@@ -267,47 +267,47 @@ of them for both the expression construct and their value counterpart. *)
Lemma
Lam_typed
Γ
x
e
τ
1
τ
2
:
binder_insert
x
τ
1
Γ
⊢
ₜ
e
:
τ
2
→
Γ
⊢
ₜ
(
λ
:
x
,
e
)
:
TArr
τ
1
τ
2
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
Lemma
LamV_typed
x
e
τ
1
τ
2
:
binder_insert
x
τ
1
∅
⊢
ₜ
e
:
τ
2
→
⊢
ᵥ
(
λ
:
x
,
e
)
:
TArr
τ
1
τ
2
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
Lemma
Let_typed
Γ
x
e1
e2
τ
1
τ
2
:
Γ
⊢
ₜ
e1
:
τ
1
→
binder_insert
x
τ
1
Γ
⊢
ₜ
e2
:
τ
2
→
Γ
⊢
ₜ
(
let
:
x
:
=
e1
in
e2
)
:
τ
2
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
Lemma
Seq_typed
Γ
e1
e2
τ
1
τ
2
:
Γ
⊢
ₜ
e1
:
τ
1
→
Γ
⊢
ₜ
e2
:
τ
2
→
Γ
⊢
ₜ
(
e1
;;
e2
)
:
τ
2
.
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
Lemma
Skip_typed
Γ
:
Γ
⊢
ₜ
Skip
:
().
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
(** * Typing of concrete programs *)
(** ** Exercise (swap_typed, easy) *)
(** Prove that the non-polymorphic swap function [swap] can be given the type
[ref τ → ref τ → ()] for any [τ]. *)
Lemma
swap_typed
τ
:
⊢
ᵥ
swap
:
(
ref
τ
→
ref
τ
→
()).
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
(** ** Exercise (swap_poly_typed, easy) *)
(** Prove that [swap_poly] can be typed using the polymorphic type
[∀ X, ref X → ref X → ())], i.e. [∀: ref #0 → ref #0 → ())] in De Bruijn style. *)
Lemma
swap_poly_typed
:
⊢
ᵥ
swap_poly
:
(
∀:
ref
#
0
→
ref
#
0
→
()).
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
(** ** Exercise (not_typed, easy) *)
(** Prove that the programs [unsafe_pure] and [unsafe_ref] from [language.v]
cannot be typed using the syntactic type system. *)
Lemma
unsafe_pure_not_typed
τ
:
¬
(
⊢
ᵥ
unsafe_pure
:
τ
).
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
Lemma
unsafe_ref_not_typed
τ
:
¬
(
⊢
ᵥ
unsafe_ref
:
τ
).
Proof
.
(* FILL IN YOUR PROOF *)
Q
ed
.
Proof
.
(* FILL IN YOUR PROOF *)
Admitt
ed
.
mk-exercises.sh
View file @
e5303d75
...
...
@@ -3,7 +3,7 @@ set -e
# config
REPLACE
=
"perl -0pe"
REMOVEPRF_RE
=
's/\(\*\s*REMOVE\s*\*\)\s*Proof.\s*.*?\s*Qed\.\R/Proof. (* FILL IN YOUR PROOF *)
Q
ed.\n/gms'
REMOVEPRF_RE
=
's/\(\*\s*REMOVE\s*\*\)\s*Proof.\s*.*?\s*Qed\.\R/Proof. (* FILL IN YOUR PROOF *)
Admitt
ed.\n/gms'
REMOVE_RE
=
's/\(\*\s*REMOVE\s*\*\)\s*(.*?)\s*:=.*?\.\R/\1. (* FILL IN HERE *) Admitted.\n/gms'
STRONGHIDE_RE
=
's/\(\*\s*STRONGHIDE\s*\*\)\s*(.*?)\(\*\s*ENDSTRONGHIDE\s*\*\)\R?//gms'
HIDE_RE
=
's/\(\*\s*HIDE\s*\*\)\s*(.*?)\(\*\s*ENDHIDE\s*\*\)/Definition hole := remove_this_line.\n(* ANSWER THE QUESTION AND REMOVE THE LINE ABOVE *)/gms'
...
...
solutions/compatibility.v
View file @
e5303d75
...
...
@@ -57,8 +57,8 @@ Section compatibility.
wp_apply
(
wp_wand
with
"(H [//])"
)
;
iIntros
(
w
).
iDestruct
1
as
(
w1
w2
->)
"[??]"
.
by
wp_pures
.
Qed
.
(* REMOVE *)
Lemma
Snd_sem_typed
Γ
e
A1
A2
:
Γ
⊨
e
:
A1
*
A2
-
∗
Γ
⊨
Snd
e
:
A2
.
Proof
.
Lemma
Snd_sem_typed
Γ
e
A1
A2
:
Γ
⊨
e
:
A1
*
A2
-
∗
Γ
⊨
Snd
e
:
A2
.
(* REMOVE *)
Proof
.
iIntros
"#H"
(
vs
)
"!# #HΓ /="
.
wp_apply
(
wp_wand
with
"(H [//])"
)
;
iIntros
(
w
).
iDestruct
1
as
(
w1
w2
->)
"[??]"
.
by
wp_pures
.
...
...
@@ -70,8 +70,8 @@ Section compatibility.
wp_apply
(
wp_wand
with
"(H [//])"
)
;
iIntros
(
w
)
"#HA"
.
wp_pures
.
iLeft
.
iExists
w
.
auto
.
Qed
.
(* REMOVE *)
Lemma
InjR_sem_typed
Γ
e
A1
A2
:
Γ
⊨
e
:
A2
-
∗
Γ
⊨
InjR
e
:
A1
+
A2
.
Proof
.
Lemma
InjR_sem_typed
Γ
e
A1
A2
:
Γ
⊨
e
:
A2
-
∗
Γ
⊨
InjR
e
:
A1
+
A2
.
(* REMOVE *)
Proof
.
iIntros
"#H"
(
vs
)
"!# #HΓ /="
.
wp_apply
(
wp_wand
with
"(H [//])"
)
;
iIntros
(
w
)
"#HA"
.
wp_pures
.
iRight
.
iExists
w
.
auto
.
...
...
solutions/sem_type_formers.v
View file @
e5303d75
...
...
@@ -7,112 +7,105 @@ formers, which given two semantic types [A] and [B], gives the semantic type of
the product [A * B], i.e., values that are pairs where the first component
belongs to [A] and the second component to [B]. *)
Section
types
.
Context
`
{!
heapG
Σ
}.
(** * Base types *)
(** Let us start with the simplest types of our language: unit and Boolean.
The corresponding semantic types are defined as follows: *)
Definition
sem_ty_unit
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
⌜
w
=
#()
⌝
)%
I
.
Definition
sem_ty_bool
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
b
:
bool
,
⌜
w
=
#
b
⌝
)%
I
.
(** These interpretations are exactly what you would expect: the only value
of the unit type is the unit value [()], the values of the Boolean type are
the elements of the Coq type [bool] (i.e. [true] and [false]). *)
(** ** Exercise (sem_ty_int, easy) *)
(** Define the semantic version of the type of integers. *)
(* REMOVE *)
Definition
sem_ty_int
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
n
:
Z
,
⌜
w
=
#
n
⌝
)%
I
.
(** * Products and sums *)
(** The semantic type former for products is as follows: *)
Definition
sem_ty_prod
(
A1
A2
:
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
w1
w2
,
⌜
w
=
(
w1
,
w2
)%
V
⌝
∧
A1
w1
∧
A2
w2
)%
I
.
(** Values of the product type over [A1] and [A2] should be tuples [(w1, w2)],
where [w1] and [w2] should values in the semantic type [A1] and [A2],
respectively. *)
(** ** Exercise (sem_ty_sum, moderate) *)
(** Define the semantic type former for sums. *)
(* REMOVE *)
Definition
sem_ty_sum
(
A1
A2
:
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
(
∃
w1
,
⌜
w
=
InjLV
w1
⌝
∧
A1
w1
)
∨
(
∃
w2
,
⌜
w
=
InjRV
w2
⌝
∧
A2
w2
))%
I
.
(** * Functions *)
(** The semantic type former for functions is as follows: *)
Definition
sem_ty_arr
(
A1
A2
:
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
□
∀
v
,
A1
v
-
∗
WP
App
w
v
{{
A2
}})%
I
.
(** This definition is very close to the usual way of defining the type
former for the function type [A1 → A2] in traditional logical relations: it
expresses that arguments of semantic type [A1] are mapped to results of
semantic type [A2]. The definition makes two of two features of Iris:
- The weakest precondition [WP e {{ Φ }}].
- The persistence modality [□]. Recall that semantic types are persistent Iris
predicates. However, even if both [P] and [Q] are persistent propositions,
the magic wand [P -∗ Q] is not necessarily persistent. Hence, we use the [□
modality to make the magic wand persistent.
*)
(** * Polymorphism and existentials *)
Definition
sem_ty_forall
(
C
:
sem_ty
Σ
→
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
□
∀
A
:
sem_ty
Σ
,
WP
w
#()
{{
w
,
C
A
w
}})%
I
.
Definition
sem_ty_exist
(
C
:
sem_ty
Σ
→
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
A
:
sem_ty
Σ
,
C
A
w
)%
I
.
(** The interpretations of these types are fairly straightforward.
Given a higher-order type former [C] that maps semantic types to
semantic types, we define the universal type [sem_ty_forall A]
using the universal quantification in Iris. That is, a value [w]
is considered a polymorphic value if for any semantic type [A],
when [w] is specialized to the type [A] (written as [w #()] as
(semantic) types never appear in terms in our untyped syntax)
the _resulting expression_ is an expression in the semantics of
the type [C A] (defined using WP).
Similarly, given a higher-order type former [C] that maps
semantic types to semantic types, we define the existential type
[sem_ty_exist A] using the existential quantification in Iris.
Notice how the impredicative nature of Iris propositions and
predicates allows us to quantify over Iris predicates to define
an Iris predicate. This is crucial for giving semantics to
parametric polymorphism, i.e., universal and existential types.
Remark: notice that for technical reasons (related to the value
restriction problem in ML-like languages) universally quantified
expressions are not evaluated until they are applied to a
specific type. *)
(** * References *)
Definition
tyN
:
=
nroot
.@
"ty"
.
Definition
sem_ty_ref
(
A
:
sem_ty
Σ
)
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
∃
l
:
loc
,
⌜
w
=
#
l
⌝
∧
inv
(
tyN
.@
l
)
(
∃
v
,
l
↦
v
∗
A
v
))%
I
.
(** Intuitively, values of the reference type [sem_ty_ref A] should
be locations [l] that hold a value [w] in the semantic type [A] at
all times. In order to express this intuition in a formal way, we
make use of two features of Iris:
- The points-to connective l ↦ v (from vanilla separation logic)
provides exclusive ownership of the location l with value
v. The points-to connective is an ephemeral proposition, and
necessarily not a persistent proposition.
- The invariant assertion [inv N P] expresses that a (typically
ephemeral) proposition [P] holds at all times -- i.e., [P] is
invariant. The invariant assertion is persistent.
*)
(** Remark: Iris is also capable giving semantics to recursive
types. However, for the sake of simplicity we did not consider
recursive types for this tutorial. In particular, to give the
semantics of recursive types one needs to use Iris's guarded
fixpoints, which require some additional bookkeeping related to
contractiveness. *)
End
types
.
(** * Base types *)
(** Let us start with the simplest types of our language: unit, Boolean, and
integers. The corresponding semantic types are defined as follows: *)
Definition
sem_ty_unit
{
Σ
}
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,
⌜
w
=
#()
⌝
)%
I
.
Definition
sem_ty_bool
{
Σ
}
:
sem_ty
Σ
:
=
SemTy
(
λ
w
,