Commit 427f1f39 authored by Robbert Krebbers's avatar Robbert Krebbers

Work, work.

parent baeb2210
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 : T1 Γ ⊢ e2 : T2
--------------------------------
Γ ⊢ (e1, e2) : T1 × T2
Γ ⊢ e1 : τ1 Γ ⊢ e2 : τ2
--------------------------------
Γ ⊢ (e1, e2) : τ1 × τ2
>>
becomes
becomes:
<<
(Γ ⊨ e1 : T1) -∗ (Γ ⊨ e2 : T2) -∗ Γ ⊢ (e1, e2) : T1 × T2
(Γ ⊨ e1 : A1) -∗ (Γ ⊨ e2 : A2) -∗ Γ ⊢ (e1, e2) : A1 * A2
>>
*)
*)
Section compatibility.
Context `{!heapG Σ}.
......
......@@ -16,7 +16,7 @@ Overview of the lecture:
Γ ⊢ₜ e : τ
2. Following Derek's talk, we define semantic typing in Iris:
2. Following Dreyer'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.
......
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 Σ}.
......
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.
(* Use [elim:] instead of [induction] so we can properly name hyps *)
(* We use [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.
(* Use [elim:] instead of [induction] so we can properly name hyps *)
(* We use [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).
......
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 well-typed 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 well-typed
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
......
From tutorial_popl20 Require Export sem_typed.
(* Typing for operators *)
(** 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 Σ}.
......
......@@ -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 := {}.
......
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 Σ))
......
......@@ -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.
......
......@@ -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))].
......
......@@ -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".
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment