Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Fengmin Zhu
Tutorial POPL20
Commits
427f1f39
Commit
427f1f39
authored
Jan 20, 2020
by
Robbert Krebbers
Browse files
Work, work.
parent
baeb2210
Changes
11
Hide whitespace changes
Inline
Sidebyside
theories/compatibility.v
View file @
427f1f39
From
tutorial_popl20
Require
Export
sem_typed
sem_operators
.
(** * Compatibility of logical relations with typing rules.
(** * Compatibility of logical relations with typing rules *)
(** We prove that the logical relations, i.e., the semantic typing judgment,
that we have defined is compatible with typing rules. That is, the logical
relations is a congruence with respect to the typing rules.
Here we prove that the logical relations, i.e., the semantic
typing judgment, that we have defined is compatible with typing
rules. That is, the logical relations is a congruence with respect
to the typing rules.
These compatibility lemmas are what one gets when the syntactic
typing judgment is replaced semantic typing judgment in syntactic
typing rules. For instance ([sem_typed_pair]):
These compatibility lemmas are what one gets when the syntactic typing judgment
is replaced semantic typing judgment in syntactic typing rules. For instance
([sem_typed_pair]):
<<
Γ ⊢ e1 :
T
1 Γ ⊢ e2 :
T
2

Γ ⊢ (e1, e2) :
T
1 ×
T
2
Γ ⊢ e1 :
τ
1 Γ ⊢ e2 :
τ
2

Γ ⊢ (e1, e2) :
τ
1 ×
τ
2
>>
becomes
becomes:
<<
(Γ ⊨ e1 :
T
1) ∗ (Γ ⊨ e2 :
T
2) ∗ Γ ⊢ (e1, e2) :
T
1
× T
2
(Γ ⊨ e1 :
A
1) ∗ (Γ ⊨ e2 :
A
2) ∗ Γ ⊢ (e1, e2) :
A
1
* A
2
>>
*)
*)
Section
compatibility
.
Context
`
{!
heapG
Σ
}.
...
...
theories/demo.v
View file @
427f1f39
...
...
@@ 16,7 +16,7 @@ Overview of the lecture:
Γ ⊢ₜ e : τ
2. Following Der
ek
's talk, we define semantic typing in Iris:
2. Following D
rey
er's talk, we define semantic typing in Iris:
Γ ⊨ e : τ
...
...
@@ 164,11 +164,10 @@ End semtyp.
Notation
"Γ ⊨ e : A"
:
=
(
sem_typed
Γ
e
A
)
(
at
level
74
,
e
,
A
at
next
level
).
Definition
safe
(
e
:
expr
)
:
=
∀
σ
es'
e'
σ
'
,
rtc
erased_step
([
e
],
σ
)
(
es'
,
σ
'
)
→
e'
∈
es'
→
is_Some
(
to_val
e'
)
∨
reducible
e'
σ
'
.
Definition
safe
(
e
:
expr
)
:
=
∀
σ
es'
e'
σ
'
,
rtc
erased_step
([
e
],
σ
)
(
es'
,
σ
'
)
→
e'
∈
es'
→
is_Some
(
to_val
e'
)
∨
reducible
e'
σ
'
.
Lemma
sem_type_safety
`
{!
heapPreG
Σ
}
e
τ
:
(
∀
`
{!
heapG
Σ
},
∅
⊨
e
:
τ
)
→
safe
e
.
...
...
theories/fundamental.v
View file @
427f1f39
From
tutorial_popl20
Require
Export
typed
compatibility
interp
.
(** * The fundamental theorem of logical relations
(** * The fundamental theorem of logical relations *)
(** The fundamental theorem of logical relations says that any syntactically
typed term is also semantically typed:
The fundamental theorem of logical relations says that any
syntactically typed term is also semantically typed:
if [Γ ⊢ e : τ] then [interp Γ ρ ⊨ e : 〚τ〛 ρ]
if [Γ ⊢ e : τ] then [interp Γ ρ ⊨ e : 〚τ〛 ρ]
Here, [ρ] is any mapping free type variables in [Γ] and [τ] to semantic types.
where [ρ] is any mapping free type variables in [Γ] and [τ] to
semantic types.
This theorem essentially follows from the compatibility lemmas by
a straightforward induction on the typing derivation. *)
This theorem essentially follows from the compatibility lemmas and an induction
on the typing derivation. *)
Section
fundamental
.
Context
`
{!
heapG
Σ
}.
...
...
theories/interp.v
View file @
427f1f39
From
tutorial_popl20
Require
Export
sem_typed
sem_type_formers
types
.
(** * Here we use semantic type formers to define semantics of syntactic types.
This is done by a straightforward induction on the syntactic type. *)
(** * Interpretation of syntactic types *)
(** We use semantic type formers to define the interpretation [⟦ τ ⟧ : sem_ty]
of syntactic types [τ : ty]. The interpretation is defined recursively on the
structure of syntactic types. *)
Reserved
Notation
"⟦ τ ⟧"
.
Fixpoint
interp
`
{!
heapG
Σ
}
(
τ
:
ty
)
(
ρ
:
list
(
sem_ty
Σ
))
:
sem_ty
Σ
:
=
...
...
@@ 22,20 +23,21 @@ where "⟦ τ ⟧" := (interp τ).
Instance
:
Params
(@
interp
)
2
:
=
{}.
(** Given a syntactic typing context [Γ] (a mapping from variables
(string) to types) together with a mapping (represented as a list)
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. *)
(** Given a syntactic typing context [Γ : gmap string ty] (a mapping from
variables [string] to syntactic types [ty]) together with a mapping
[ρ : list (sem_ty Σ)] from type variables (that appear freely in [Γ]) to
their corresponding semantic types (represented as a list, since de use De
Bruijn indices for type variables), we define a semantic typing context
[interp_env Γ ρ : gmap string (sem_ty Σ)], i.e., a mapping from variables
(strings) to semantic types. *)
Definition
interp_env
`
{!
heapG
Σ
}
(
Γ
:
gmap
string
ty
)
(
ρ
:
list
(
sem_ty
Σ
))
:
gmap
string
(
sem_ty
Σ
)
:
=
flip
interp
ρ
<$>
Γ
.
Instance
:
Params
(@
interp_env
)
3
:
=
{}.
(** Below we prove several useful lemmas about [interp] and
[interp_env] including important lemmas about the effect that
lifting (de Bruij indices) and substitution in type level
variables have on the interpretation of syntactic types and typing
contexts. *)
(** Below we prove several useful lemmas about [interp] and [interp_env],
including important lemmas about the effect that lifting (de Bruijn indices)
and substitution in type level variables have on the interpretation of syntactic
types and typing contexts. *)
Section
interp_properties
.
Context
`
{!
heapG
Σ
}.
Implicit
Types
Γ
:
gmap
string
ty
.
...
...
@@ 62,7 +64,7 @@ Section interp_properties.
n
≤
length
ρ
→
⟦
ty_lift
n
τ
⟧
ρ
≡
⟦
τ
⟧
(
delete
n
ρ
).
Proof
.
(*
U
se [elim:] instead of [induction] so we can properly name hyps *)
(*
We u
se [elim:] instead of [induction] so we can properly name hyps *)
revert
n
ρ
.
elim
:
τ
;
simpl
;
try
(
intros
;
done

f_equiv
/=
;
by
auto
).

intros
x
n
ρ
?.
repeat
case_decide
;
simplify_eq
/=
;
try
lia
.
+
by
rewrite
lookup_delete_lt
.
...
...
@@ 88,7 +90,7 @@ Section interp_properties.
i
≤
length
ρ
→
⟦
ty_subst
i
τ
'
τ
⟧
ρ
≡
⟦
τ
⟧
(
take
i
ρ
++
⟦
τ
'
⟧
ρ
::
drop
i
ρ
).
Proof
.
(*
U
se [elim:] instead of [induction] so we can properly name hyps *)
(*
We u
se [elim:] instead of [induction] so we can properly name hyps *)
revert
i
τ
'
ρ
.
elim
:
τ
;
simpl
;
try
(
intros
;
done

f_equiv
/=
;
by
auto
).

intros
x
i
τ
'
ρ
?.
repeat
case_decide
;
simplify_eq
/=
;
try
lia
.
+
rewrite
lookup_app_l
;
last
(
rewrite
take_length
;
lia
).
...
...
theories/safety.v
View file @
427f1f39
From
iris
.
heap_lang
Require
Export
adequacy
.
From
tutorial_popl20
Require
Export
fundamental
.
(** * Safety of semantic types and type safety based on that
(** * Semantic and syntactic type safety *)
(** We prove that any _closed_ expression that is semantically typed is safe,
i.e., it does not crash. Based on this theorem we then prove _syntactic type
safety_, i.e., any _closed_ syntactically welltyped program is safe. Semantic
type safety is a consequence of Iris's adequacy theorem, and syntactic type
safety is a consequence of the fundamental theorem of logical relations together
with the safety for semantic typing. *)
We prove that any _closed_ expression that is semantically typed
is safe, i.e., it does not crash. Based on this theorem we then
prove _type safety_, i.e., any _closed_ syntactically welltyped
program does not get stuck. Type safety is a simple consequence of
the fundamental theorem of logical relations together with the
safety for semantic typing.
*)
(** The following lemma states that given a closed program [e], heap
[σ], and _Coq_ predicate [φ : val → Prop], if there is a semantic
type [A] such that [A] implies [φ], and [e] is semantically typed
at type [A], then we have [adequate NotStuck e σ (λ v σ, φ
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]. *)
(** ** Semantic type safety *)
(** The following lemma states that given a closed program [e], heap [σ], and
_Coq_ predicate [φ : val → Prop], if there is a semantic type [A] such that [A]
implies [φ], and [e] is semantically typed at type [A], then we have
[adequate NotStuck e σ (λ v σ, φ 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
)%
I
)
→
adequate
NotStuck
e
σ
(
λ
v
σ
,
φ
v
).
...
...
@@ 31,9 +28,8 @@ Proof.
by
iIntros
;
iApply
HA
.
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. *)
(** 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
)%
I
)
→
rtc
erased_step
([
e
],
σ
)
(
es
,
σ
'
)
→
e'
∈
es
→
...
...
@@ 44,6 +40,7 @@ Proof.
specialize
(
Hty
_
)
as
[
A
Hty
]
;
eauto
.
Qed
.
(** ** Syntactic type safety *)
Lemma
type_safety
e
σ
es
σ
'
e'
τ
:
(
∅
⊢
ₜ
e
:
τ
)
→
rtc
erased_step
([
e
],
σ
)
(
es
,
σ
'
)
→
e'
∈
es
→
...
...
theories/sem_operators.v
View file @
427f1f39
From
tutorial_popl20
Require
Export
sem_typed
.
(*
Typing for
operator
s
*)
(*
* Semantic
operator
typing
*)
Class
SemTyUnboxed
`
{!
heapG
Σ
}
(
A
:
sem_ty
Σ
)
:
=
sem_ty_unboxed
v
:
A
v

∗
⌜
val_is_unboxed
v
⌝
.
sem_ty_unboxed
v
:
A
v

∗
⌜
val_is_unboxed
v
⌝
.
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
.
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
Σ
)
:
=
sem_ty_bin_op
v1
v2
:
A1
v1

∗
A2
v2

∗
∃
w
,
⌜
bin_op_eval
op
v1
v2
=
Some
w
⌝
∧
B
w
.
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
Σ
}.
...
...
theories/sem_type_formers.v
View file @
427f1f39
...
...
@@ 115,7 +115,7 @@ Notation "∃ A1 .. An , C" :=
(
sem_ty_exist
(
λ
A1
,
..
(
sem_ty_exist
(
λ
An
,
C
%
sem_ty
))
..))
:
sem_ty_scope
.
Notation
"'ref' A"
:
=
(
sem_ty_ref
A
)
:
sem_ty_scope
.
(** A [Params t n] instance tells Coq's setoid rewriting mechanism
_
not
_
to
(** 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
:
=
{}.
...
...
theories/sem_typed.v
View file @
427f1f39
From
tutorial_popl20
Require
Export
sem_type_formers
.
(** * Here we define the semantic typing judgment. *)
(** We define the judgment [Γ ⊨ e : A] for semantic typing of the
expression [e] at semantic type [A], assuming that free variables
in [e] belong to the semantic types described by [Γ]. This notion
is defined as follows:
 We define the semantic typing relation [env_sem_typed] for
typing contexts: An environments (mappings from free variables
to values) [vs] is in the semantic type for a typing context
[Γ], [env_sem_typed Γ vs], if for any free variable [x], [vs(x)]
is in the semantic type [Γ(x)].
 The semantic typing judgment [Γ ⊨ e : A] holds if for any
environment [vs] such that [env_sem_typed Γ vs] we have that
[subst_map vs e] is an expression in the semantics of type [A],
i.e., [WP subst_map vs e {{ A }}] holds. *)
(** * The semantic typing judgment *)
(** We define the judgment [Γ ⊨ e : A] for semantic typing of the expression [e]
at semantic type [A], assuming that free variables in [e] belong to the semantic
types described by [Γ]. This notion is defined as follows:
 We define the semantic typing relation [env_sem_typed] for typing contexts:
An environments (mappings from free variables to values) [vs] is in the
semantic type for a typing context [Γ], [env_sem_typed Γ vs], if for any free
variable [x], [vs(x)] is in the semantic type [Γ(x)].
 The semantic typing judgment [Γ ⊨ e : A] holds if for any environment [vs]
such that [env_sem_typed Γ vs] we have that [subst_map vs e] is an expression
in the semantics of type [A], i.e., [WP subst_map vs e {{ A }}] holds. *)
(** The semantic type for the typing context (environment). *)
Definition
env_sem_typed
`
{!
heapG
Σ
}
(
Γ
:
gmap
string
(
sem_ty
Σ
))
...
...
theories/symbol_ghost.v
View file @
427f1f39
...
...
@@ 2,7 +2,18 @@ From iris.algebra Require Import auth.
From
iris
.
base_logic
Require
Import
lib
.
own
.
From
iris
.
proofmode
Require
Export
tactics
.
(* The required ghost theory *)
(** * Ghost theory for the [unsafe_symbol_adt] exercise *)
(** This file defines the ghost resources [counter] and [symbol] using Iris's
generic mechanism for ghost state. These resources satisfy the following laws:
<<
counter_alloc: ==> ∃ γ, counter γ n
counter_exclusive: counter γ n1 ∗ counter γ n2 ∗ False
counter_inc: counter γ n ==∗ counter γ (S n) ∗ symbol γ n
symbol_obs: counter γ n ∗ symbol γ s ∗ ⌜(s < n)%nat⌝
>>
*)
Class
symbolG
Σ
:
=
{
symbol_inG
:
>
inG
Σ
(
authR
mnatUR
)
}.
Definition
symbol
Σ
:
gFunctors
:
=
#[
GFunctor
(
authR
mnatUR
)].
...
...
@@ 20,10 +31,6 @@ Section symbol_ghost.
Global
Instance
symbol_timeless
γ
n
:
Timeless
(
symbol
γ
n
).
Proof
.
apply
_
.
Qed
.
Lemma
counter_exclusive
γ
n1
n2
:
counter
γ
n1

∗
counter
γ
n2

∗
False
.
Proof
.
apply
bi
.
wand_intro_r
.
rewrite

own_op
own_valid
/=.
by
iDestruct
1
as
%[].
Qed
.
Global
Instance
symbol_persistent
γ
n
:
Persistent
(
symbol
γ
n
).
Proof
.
apply
_
.
Qed
.
...
...
@@ 34,6 +41,11 @@ Section symbol_ghost.
iExists
γ
.
by
iFrame
.
Qed
.
Lemma
counter_exclusive
γ
n1
n2
:
counter
γ
n1

∗
counter
γ
n2

∗
False
.
Proof
.
apply
bi
.
wand_intro_r
.
rewrite

own_op
own_valid
/=.
by
iDestruct
1
as
%[].
Qed
.
Lemma
counter_inc
γ
n
:
counter
γ
n
==
∗
counter
γ
(
S
n
)
∗
symbol
γ
n
.
Proof
.
rewrite

own_op
.
...
...
theories/two_state_ghost.v
View file @
427f1f39
...
...
@@ 2,7 +2,18 @@ From iris.algebra Require Import auth.
From
iris
.
base_logic
Require
Import
lib
.
own
.
From
iris
.
proofmode
Require
Export
tactics
.
(* The required ghost theory *)
(** * Ghost theory for the [unsafe_ref_reuse] exercise *)
(** This file defines the ghost resources [two_state_auth] and [two_state_final]
using Iris's generic mechanism for ghost state. These resources satisfy the
following laws:
<<
two_state_init: ==> ∃ γ, two_state_auth γ false
two_state_update: two_state_auth γ b ==∗ two_state_auth γ true ∗ two_state_final γ.
two_state_agree: two_state_auth γ b ∗ two_state_final γ ∗ ⌜b = true⌝.
>>
*)
Class
two_stateG
Σ
:
=
{
two_state_inG
:
>
inG
Σ
(
authR
(
optionUR
unitR
))
}.
Definition
two_state
Σ
:
gFunctors
:
=
#[
GFunctor
(
authR
(
optionUR
unitR
))].
...
...
theories/unsafe.v
View file @
427f1f39
...
...
@@ 18,7 +18,7 @@ Section unsafe.
by
iExists
13
.
Qed
.
(** * Exercise (easy) *)
(** * Exercise (
unsafe_ref,
easy) *)
(** Recall the following function we defined in the file [language.v]:
<<
Definition unsafe_ref : val := λ: <>,
...
...
@@ 34,7 +34,7 @@ Section unsafe.
by
iExists
true
.
Qed
.
(** * Exercise (moderate) *)
(** * Exercise (
unsafe_ref_ne_0,
moderate) *)
Definition
unsafe_ref_ne_0
:
val
:
=
λ
:
<>,
let
:
"l"
:
=
ref
#
1
in
((
λ
:
"x"
,
if
:
"x"
≠
#
0
then
"l"
<
"x"
else
#()),
...
...
@@ 82,7 +82,7 @@ Section unsafe.
by
wp_op
.
Qed
.
(** * Exercise (hard) *)
(** * Exercise (
unsafe_ref_reuse,
hard) *)
Definition
unsafe_ref_reuse
:
val
:
=
λ
:
<>,
let
:
"l"
:
=
ref
#
0
in
λ
:
<>,
"l"
<
#
true
;;
!
"l"
.
...
...
@@ 115,7 +115,7 @@ Section unsafe.
rewrite
/
sem_ty_car
/=.
by
iExists
_
.
Qed
.
(** * Exercise (hard) *)
(** * Exercise (
unsafe_symbol_adt,
hard) *)
(** Semantic typing of a symbol ADT (taken from Dreyer's POPL'18 talk) *)
Definition
symbol_adt_inc
:
val
:
=
λ
:
"x"
<>,
FAA
"x"
#
1
.
Definition
symbol_adt_check
:
val
:
=
λ
:
"x"
"y"
,
assert
:
"y"
<
!
"x"
.
...
...
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