Commit b2b410d9 authored by Ralf Jung's avatar Ralf Jung
Browse files

auto-generate exercises from solutions

parent db028517
......@@ -28,10 +28,12 @@ _*_.tex
*.glob
*.v.d
*.vio
Makefile.coq*
Makefile.coq
Makefile.coq.conf
.Makefile.coq.d
*.crashcoqide
.coqdeps.d
.lia.cache
build-dep
_opam
.lia.cache
......
......@@ -5,6 +5,7 @@ stages:
variables:
CPU_CORES: "10"
MAKE_TARGET: "ci"
.template: &template
stage: build
......
# Generate an exercise for each solution.
SOLUTIONS := $(wildcard solutions/*.v)
EXERCISES := $(addprefix exercises/,$(notdir $(SOLUTIONS)))
exercises: $(EXERCISES)
.PHONY: exercises
$(EXERCISES): exercises/%.v: solutions/%.v gen-exercises.awk
$(HIDE)echo "Generating exercise file $@ from $<"
$(HIDE)gawk -f gen-exercises.awk < $< > $@
# CI make target
ci: all
+@make -B exercises # force make (in case exercise files have been edited directly)
if [ -n "$$(git status --porcelain)" ]; then echo 'ERROR: Exercise files are not up-to-date with solutions. `git diff` after re-making them:'; git diff; exit 1; fi
......@@ -100,3 +100,35 @@ If you would like to know more about Iris, we recommend to take a look at:
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars
Birkedal, Derek Dreyer.
A detailed description of the Iris logic and its model
## Generating the exercises
If you want to contribute to the tutorial, note that the files in `exercises/`
are generated from the corresponding files in `solutions/`. Run `make exercises`
to re-generate those files. This requires `gawk` to be installed (which should
usually be available on Linux but might have to be installed separately on
macOS).
The syntax for the solution files is as follows:
```
(* BEGIN SOLUTION *)
solution here.
(* END SOLUTION *)
```
is replaced by
```
(* exercise *)
Admitted.
```
and the more powerful
```
(* BEGIN SOLUTION *)
solution here.
(* END SOLUTION BEGIN TEMPLATE
exercise template here.
END TEMPLATE *)
```
is replaced by
```
exercise template here.
```
......@@ -58,16 +58,24 @@ 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. (* FILL IN YOUR PROOF *) Admitted.
Proof.
(* exercise *)
Admitted.
Lemma InjL_sem_typed Γ e A1 A2 : Γ e : A1 - Γ InjL e : A1 + A2.
Proof. (* FILL IN YOUR PROOF *) Admitted.
Proof.
(* exercise *)
Admitted.
Lemma InjR_sem_typed Γ e A1 A2 : Γ e : A2 - Γ InjR e : A1 + A2.
Proof. (* FILL IN YOUR PROOF *) Admitted.
Proof.
(* exercise *)
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 *) Admitted.
Proof.
(* exercise *)
Admitted.
(** * Functions *)
Lemma Rec_sem_typed Γ f x e A1 A2 :
......@@ -101,11 +109,15 @@ Section compatibility.
Qed.
Lemma Pack_sem_typed Γ e C A : Γ e : C A - Γ (pack: e) : A, C A.
Proof. (* FILL IN YOUR PROOF *) Admitted.
Proof.
(* exercise *)
Admitted.
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 *) Admitted.
Proof.
(* exercise *)
Admitted.
(** ** Heap operations *)
Lemma Alloc_sem_typed Γ e A : Γ e : A - Γ ref e : ref A.
......@@ -126,15 +138,21 @@ Section compatibility.
Qed.
Lemma Store_sem_typed Γ e1 e2 A :
Γ e1 : ref A - Γ e2 : A - Γ (e1 <- e2) : ().
Proof. (* FILL IN YOUR PROOF *) Admitted.
Proof.
(* exercise *)
Admitted.
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 *) Admitted.
Proof.
(* exercise *)
Admitted.
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 *) Admitted.
Proof.
(* exercise *)
Admitted.
(** ** Operators *)
Lemma UnOp_sem_typed Γ e op A B :
......@@ -146,16 +164,22 @@ 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 *) Admitted.
Proof.
(* exercise *)
Admitted.
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 *) Admitted.
Proof.
(* exercise *)
Admitted.
(** ** Fork *)
Lemma Fork_sem_typed Γ e : Γ e : () - Γ Fork e : ().
Proof. (* FILL IN YOUR PROOF *) Admitted.
Proof.
(* exercise *)
Admitted.
(** * Compatibility rules for value typing *)
(** ** Base types *)
......@@ -164,7 +188,9 @@ Section compatibility.
Lemma BoolV_sem_typed (b : bool) : #b : sem_ty_bool.
Proof. by iExists b. Qed.
Lemma IntV_sem_typed (n : Z) : #n : sem_ty_int.
Proof. (* FILL IN YOUR PROOF *) Admitted.
Proof.
(* exercise *)
Admitted.
(** ** Products and sums *)
Lemma PairV_sem_typed v1 v2 τ1 τ2 :
......
From exercises Require Import language.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import adequacy.
(**
Overview of the lecture:
1. HeapLang is an untyped language. We first define syntactic types and a
syntactic typing judgment.
Γ ⊢ₜ e : τ
2. Following Dreyer's talk, we define semantic typing in Iris:
Γ ⊨ e : τ
3. We then prove the fundamental theorem:
Γ ⊢ₜ e : τ → Γ ⊨ e : τ
Every term that is syntactically typed, is also semantically typed
4. We prove safety of semantic typing:
∅ ⊨ e : τ → e is safe, i.e. cannot crash
5. We prove that we get more by showing that certain "unsafe" programs are also
semantically typed
*)
Inductive ty :=
| TUnit : ty
| TBool : ty
| TInt : ty
| TProd : ty ty ty
| TArr : ty ty ty
| TRef : ty ty.
Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
Inductive typed : gmap string ty expr ty Prop :=
(** Variables *)
| Var_typed Γ x τ :
Γ !! x = Some τ
Γ Var x : τ
(** Base values *)
| UnitV_typed Γ :
Γ #() : TUnit
| BoolV_typed Γ (b : bool) :
Γ #b : TBool
| IntV_val_typed Γ (i : Z) :
Γ #i : TInt
(** Products *)
| Pair_typed Γ e1 e2 τ1 τ2 :
Γ e1 : τ1 Γ e2 : τ2
Γ Pair e1 e2 : TProd τ1 τ2
| Fst_typed Γ e τ1 τ2 :
Γ e : TProd τ1 τ2
Γ Fst e : τ1
| Snd_typed Γ e τ1 τ2 :
Γ e : TProd τ1 τ2
Γ Snd e : τ2
(** Functions *)
| Rec_typed Γ f x e τ1 τ2 :
binder_insert f (TArr τ1 τ2) (binder_insert x τ1 Γ) e : τ2
Γ Rec f x e : TArr τ1 τ2
| App_typed Γ e1 e2 τ1 τ2 :
Γ e1 : TArr τ1 τ2 Γ e2 : τ1
Γ App e1 e2 : τ2
(** Heap operations *)
| Alloc_typed Γ e τ :
Γ e : τ
Γ Alloc e : TRef τ
| Load_typed Γ e τ :
Γ e : TRef τ
Γ Load e : τ
| Store_typed Γ e1 e2 τ :
Γ e1 : TRef τ Γ e2 : τ
Γ Store e1 e2 : TUnit
(** If *)
| If_typed Γ e0 e1 e2 τ :
Γ e0 : TBool Γ e1 : τ Γ e2 : τ
Γ If e0 e1 e2 : τ
where "Γ ⊢ₜ e : τ" := (typed Γ e τ).
Section semtyp.
Context `{!heapG Σ}.
Record sem_ty := SemTy {
sem_ty_car :> val iProp Σ;
sem_ty_persistent v : Persistent (sem_ty_car v)
}.
Arguments SemTy _%I {_}.
Existing Instance sem_ty_persistent.
Fixpoint interp (τ : ty) : sem_ty :=
match τ with
| TUnit => SemTy (λ w, w = #())
| TBool => SemTy (λ w, w = #true w = #false)
| TInt => SemTy (λ w, i : Z, w = #i)
| TProd τ1 τ2 =>
SemTy (λ w, w1 w2, w = (w1, w2)%V interp τ1 w1 interp τ2 w2)
| TArr τ1 τ2 =>
SemTy (λ w, v, interp τ1 v - WP w v {{ u, interp τ2 u }})
| TRef τ =>
SemTy
(λ w, l : loc, w = #l inv (nroot .@ l) ( v, l v interp τ v))
end%I.
Definition interp_env (Γ : gmap string ty) (vs : gmap string val) : iProp Σ :=
[ map] τ;v Γ;vs, interp τ v.
Definition sem_typed (Γ : gmap string ty) (e : expr) (τ : ty) : iProp Σ :=
vs : gmap string val,
interp_env Γ vs - WP subst_map vs e {{ w, interp τ w }}.
Notation "Γ ⊨ e : A" := (sem_typed Γ e A)
(at level 74, e, A at next level).
Theorem fundamental Γ e τ : Γ e : τ Γ e : τ.
Proof. Admitted.
End semtyp.
Notation "Γ ⊨ e : A" := (sem_typed Γ e A)
(at level 74, e, A at next level).
......@@ -233,7 +233,9 @@ 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 *) Admitted.
Proof.
(* exercise *)
Admitted.
(** ** Reasoning about higher-order functions *)
(** For the next example, let us consider the higher-order function [twice].
......@@ -336,7 +338,9 @@ 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 *) Admitted.
Proof.
(* exercise *)
Admitted.
(** ** Reasoning about higher-order state *)
(** To see how Iris can be used to reason about higher-order state---that is,
......@@ -407,7 +411,9 @@ Definition add_two_fancy : val := λ: "x",
Lemma wp_add_two_fancy `{!heapG Σ} (x : Z) :
WP add_two_fancy #x {{ w, w = #(2 + x) }}.
Proof. (* FILL IN YOUR PROOF *) Admitted.
Proof.
(* exercise *)
Admitted.
(** * Reasoning about "unsafe" programs *)
(** Since HeapLang is an untyped language, we can write down arbitrary
......@@ -438,4 +444,6 @@ Definition unsafe_ref : val := λ: <>,
Lemma wp_unsafe_ref `{!heapG Σ} :
WP unsafe_ref #() {{ v, v = #true }}.
Proof. (* FILL IN YOUR PROOF *) Admitted.
Proof.
(* exercise *)
Admitted.
......@@ -27,20 +27,26 @@ Section parametricity.
( `{!heapG Σ}, e : A, A)
rtc erased_step ([e <_>]%E, σ) (of_val w :: es, σ')
False.
Proof. (* FILL IN YOUR PROOF *) Admitted.
Proof.
(* exercise *)
Admitted.
(** * Exercise (boolean_param, moderate) *)
Lemma boolean_param `{!heapPreG Σ} e (v1 v2 : val) σ w es σ' :
( `{!heapG Σ}, e : A, A A A)
rtc erased_step ([e <_> v1 v2]%E, σ) (of_val w :: es, σ') w = v1 w = v2.
Proof. (* FILL IN YOUR PROOF *) Admitted.
Proof.
(* exercise *)
Admitted.
(** * Exercise (nat_param, hard) *)
Lemma nat_param `{!heapPreG Σ} e σ w es σ' :
( `{!heapG Σ}, e : A, (A A) A A)
rtc erased_step ([e <_> (λ: "n", "n" + #1)%V #0]%E, σ)
(of_val w :: es, σ') n : nat, w = #n.
Proof. (* FILL IN YOUR PROOF *) Admitted.
Proof.
(* exercise *)
Admitted.
(** * Exercise (strong_nat_param, hard) *)
Lemma strong_nat_param `{!heapPreG Σ} e σ w es σ' (vf vz : val) φ :
......@@ -50,5 +56,7 @@ Section parametricity.
( Φ vz)
( w, Φ w - ⌜φ w))
rtc erased_step ([e <_> vf vz]%E, σ) (of_val w :: es, σ') φ w.
Proof. (* FILL IN YOUR PROOF *) Admitted.
Proof.
(* exercise *)
Admitted.
End parametricity.
......@@ -44,4 +44,6 @@ 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 *) Admitted.
Proof.
(* exercise *)
Admitted.
......@@ -267,47 +267,65 @@ 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 *) Admitted.
Proof.
(* exercise *)
Admitted.
Lemma LamV_typed x e τ1 τ2 :
binder_insert x τ1 e : τ2
(λ: x, e) : TArr τ1 τ2.
Proof. (* FILL IN YOUR PROOF *) Admitted.
Proof.
(* exercise *)
Admitted.
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 *) Admitted.
Proof.
(* exercise *)
Admitted.
Lemma Seq_typed Γ e1 e2 τ1 τ2 :
Γ e1 : τ1
Γ e2 : τ2
Γ (e1;; e2) : τ2.
Proof. (* FILL IN YOUR PROOF *) Admitted.
Proof.
(* exercise *)
Admitted.
Lemma Skip_typed Γ :
Γ Skip : ().
Proof. (* FILL IN YOUR PROOF *) Admitted.
Proof.
(* exercise *)
Admitted.
(** * 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 *) Admitted.
Proof.
(* exercise *)
Admitted.
(** ** 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 *) Admitted.
Proof.
(* exercise *)
Admitted.
(** ** 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 *) Admitted.
Proof.
(* exercise *)
Admitted.
Lemma unsafe_ref_not_typed τ : ¬ ( unsafe_ref : τ).
Proof. (* FILL IN YOUR PROOF *) Admitted.
Proof.
(* exercise *)
Admitted.
BEGIN {
in_solution = 0;
}
{ # on every line of the input
if (match($0, /^( *)\(\* *BEGIN SOLUTION *\*\)$/, groups)) {
in_solution = 1
} else if (match($0, /^( *)\(\* *END SOLUTION *\*\)$/, groups)) {
print groups[1] " (* exercise *)"
print groups[1] "Admitted."
in_solution = 0
} else if (match($0, /^( *)\(\* *END SOLUTION BEGIN TEMPLATE *$/, groups)) {
in_solution = 0
} else if (match($0, /^( *)END TEMPLATE *\*\)$/, groups)) {
# Nothing to do, just do not print this line.
} else if (in_solution == 0) {
gsub("From solutions Require", "From exercises Require")
print
}
}
......@@ -58,28 +58,35 @@ Section compatibility.
iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures.
Qed.
Lemma Snd_sem_typed Γ e A1 A2 : Γ e : A1 * A2 - Γ Snd e : A2.
(* REMOVE *) Proof.
Proof.
(* BEGIN SOLUTION *)
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w).
iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures.
Qed.
(* END SOLUTION *)
Lemma InjL_sem_typed Γ e A1 A2 : Γ e : A1 - Γ InjL e : A1 + A2.
(* REMOVE *) Proof.
Proof.
(* BEGIN SOLUTION *)
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HA".
wp_pures. iLeft. iExists w. auto.
Qed.
(* END SOLUTION *)
Lemma InjR_sem_typed Γ e A1 A2 : Γ e : A2 - Γ InjR e : A1 + A2.
(* REMOVE *) Proof.
Proof.
(* BEGIN SOLUTION *)
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HA".
wp_pures. iRight. iExists w. auto.
Qed.
(* END SOLUTION *)
Lemma Case_sem_typed Γ e e1 e2 A1 A2 B :
Γ e : A1 + A2 - Γ e1 : (A1 B) - Γ e2 : (A2 B) -
Γ Case e e1 e2 : B.
(* REMOVE *) Proof.
Proof.
(* BEGIN SOLUTION *)
iIntros "#H #H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#[HA|HA]".
- iDestruct "HA" as (w1 ->) "HA". wp_pures.
......@@ -87,6 +94,7 @@ Section compatibility.
- iDestruct "HA" as (w2 ->) "HA". wp_pures.
wp_apply (wp_wand with "(H2 [//])"); iIntros (v) "#HAB". by iApply "HAB".
Qed.
(* END SOLUTION *)
(** * Functions *)
Lemma Rec_sem_typed Γ f x e A1 A2 :
......@@ -120,15 +128,18 @@ Section compatibility.
Qed.
Lemma Pack_sem_typed Γ e C A : Γ e : C A - Γ (pack: e) : A, C A.
(* REMOVE *) Proof.
Proof.
(* BEGIN SOLUTION *)
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB".
wp_lam. by iExists A.
Qed.