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

Merge branch 'ralf/auto-exercises' into 'master'

Auto-generate exercise files

See merge request iris/tutorial-popl20!2
parents db028517 5b508c95
......@@ -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
......@@ -74,11 +74,6 @@ Ghost theory for semantic safety of "unsafe" programs:
- [symbol_ghost.v](exercises/symbol_ghost.v): The ghost theory for the symbol
ADT example.
Other:
- [demo.v](exercises/demo.v): A simplified version of the development to the
simplified case, as shown during the lecture at the POPL'20 tutorial.
## Documentation
The files [proof_mode.md] and [heap_lang.md] in the Iris repository contain a
......@@ -100,3 +95,36 @@ 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:
```
(* SOLUTION *) Proof.
solution here.
Qed.
```
is replaced by
```
Proof.
(* 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.
(** This file contains a simplified version of the development that we used
throughout the lectures. This simplified version contains a subset of the
features in the full version. Notably, it does not support unary and binary
operators, sums, polymorphic functions, and existential types. Moreover, in
this version, we define the interpretation of types [interp] in a direct style,
instead of using semantic type formers as combinators on [sem_ty].
Overview of the lecture:
1. HeapLang is a untyped language. We first define a 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, n : Z, w = #n )
| TProd τ1 τ2 =>
SemTy (λ w, v1 v2, w = (v1, v2)%V interp τ1 v1 interp τ2 v2)
| 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 .@ "ref" .@ 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, 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).
Lemma Pair_sem_typed Γ e1 e2 τ1 τ2 :
Γ e1 : τ1 - Γ e2 : τ2 - Γ Pair e1 e2 : TProd τ1 τ2.
Proof.
iIntros "#He1 #He2".
rewrite /sem_typed.
iIntros "!#".
iIntros (vs) "#Hvs".
simpl.
wp_bind (subst_map vs e2).
iApply wp_wand.
{ by iApply "He2". }
iIntros (w2) "Hw2".
wp_bind (subst_map vs e1).
iApply wp_wand.
{ by iApply "He1". }
iIntros (w1) "Hw1".
wp_pures.
iExists w1, w2. iFrame. auto.
Restart.
iIntros "#He1 #He2 !#" (vs) "#Hvs /=".
wp_apply (wp_wand with "(He2 [$])").
iIntros (w2) "Hw2".
wp_apply (wp_wand with "(He1 [$])").
iIntros (w1) "Hw1".
wp_pures; eauto.
Qed.
Theorem fundamental Γ e τ : Γ e : τ Γ e : τ.
Proof.
intros Htyped. iInduction Htyped as [] "IH".
5:{ iApply Pair_sem_typed; auto. }
(** Other cases left as an exercise to the reader *)
Admitted.
Lemma sem_typed_unsafe_pure :
(if: #true then #13 else #13 #37) : TInt.
Proof.
iIntros "!#" (vs) "Hvs /=". wp_pures. auto.
Qed.
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' σ'.
Lemma sem_type_safety `{!heapPreG Σ} e τ :
( `{!heapG Σ}, e : τ) safe e.
Proof.
intros Hty σ es' e' σ'.
apply (heap_adequacy Σ NotStuck e σ (λ _, True))=> // ?.
iDestruct (Hty $! ) as "#He".
rewrite subst_map_empty. iApply (wp_wand with "(He [])").
{ rewrite /interp_env. auto. }
auto.
Qed.
Lemma type_safety e τ : e : τ safe e.
Proof.
intros Hty. eapply (sem_type_safety (Σ:=heapΣ))=> ?.
by apply fundamental.
Qed.
......@@ -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; # for the advanced solution syntax
in_auto_solution = 0; # for the simple solution syntax that recognizes `Qed.`
}
{ # on every line of the input
if (match($0, /^( *)\(\* *SOLUTION *\*\) *Proof.$/, groups)) {
print groups[1] "Proof."
in_auto_solution = 1
} else if (in_auto_solution == 1 && match($0, /^( *)Qed.$/, groups)) {
print groups[1] " (* exercise *)"
print groups[1] "Admitted."
in_auto_solution = 0
} else if (match($0, /^( *)\(\* *BEGIN SOLUTION *\*\)$/, groups)) {
in_solution = 1
} 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 && in_auto_solution == 0) {
gsub("From solutions Require", "From exercises Require")
print
}
}
......@@ -58,20 +58,20 @@ 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.
(* SOLUTION *) Proof.