README.md 4.68 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
# The Iris tutorial @ POPL'20

This tutorial comes in two versions:

Robbert Krebbers's avatar
Robbert Krebbers committed
5
6
- The folder [exercises](exercises): skeletons of the exercises with solutions left out.
- The folder [solutions](solutions): the exercises together with their solutions.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
9
10
11

## Dependencies

For the tutorial material you need to have the following dependencies installed:

Ralf Jung's avatar
Ralf Jung committed
12
- Coq 8.11.2 / 8.12.0
Ralf Jung's avatar
add CI    
Ralf Jung committed
13
- [Iris](https://gitlab.mpi-sws.org/iris/iris) 3.3.0
Robbert Krebbers's avatar
Robbert Krebbers committed
14
15
16
17
18
19
20
21

*Note:* the tutorial material will not work with earlier versions of Iris, it
is important to install the exact versions as given above.

## Installing Iris via opam

The easiest, and recommend, way of installing Iris and its dependencies is via
the OCaml package manager opam (2.0.0 or newer). You first have to add the Coq
22
opam repository (if you have not already done so earlier):
Robbert Krebbers's avatar
Robbert Krebbers committed
23
24
25
26
27
28
29
30
31
32
33
34
35

    opam repo add coq-released https://coq.inria.fr/opam/released

Then you can do `make build-dep` to install exactly the right version of Iris.

## Compiling the exercises

Run `make` to compile the exercises.

## Overview

Introduction to Iris and the HeapLang language:

Robbert Krebbers's avatar
Robbert Krebbers committed
36
- [language.v](exercises/language.v): An introduction to Iris's HeapLang
Robbert Krebbers's avatar
Robbert Krebbers committed
37
38
  language, program specifications using weakest preconditions, and proofs of
  these specifications using Iris's tactics for separation logic.
Robbert Krebbers's avatar
Robbert Krebbers committed
39
- [polymorphism.v](exercises/polymorphism.v): The encoding of polymorphic
Robbert Krebbers's avatar
Robbert Krebbers committed
40
41
42
43
  functions and existential packages in HeapLang.

Syntactic typing:

Robbert Krebbers's avatar
Robbert Krebbers committed
44
- [types.v](exercises/types.v): The definition of syntactic types and the
Robbert Krebbers's avatar
Robbert Krebbers committed
45
  type-level substitution function.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
- [typed.v](exercises/typed.v): The syntactic typing judgment.
Robbert Krebbers's avatar
Robbert Krebbers committed
47
48
49

Semantic typing:

Robbert Krebbers's avatar
Robbert Krebbers committed
50
51
- [sem_types.v](exercises/sem_types.v): The model of semantic types in Iris.
- [sem_typed.v](exercises/sem_typed.v): The definition of the semantic typing
Robbert Krebbers's avatar
Robbert Krebbers committed
52
  judgment in Iris.
Robbert Krebbers's avatar
Robbert Krebbers committed
53
- [sem_type_formers.v](exercises/sem_type_formers.v): The definition of the
Robbert Krebbers's avatar
Robbert Krebbers committed
54
55
  semantic counterparts of the type formers (like products, sums, functions,
  references, etc.).
Robbert Krebbers's avatar
Robbert Krebbers committed
56
- [sem_operators.v](exercises/sem_operators.v): The judgment for semantic
Robbert Krebbers's avatar
Robbert Krebbers committed
57
  operator typing and proofs of the corresponding semantic rules.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
- [compatibility.v](exercises/compatibility.v): The semantic typing rules, i.e.,
Robbert Krebbers's avatar
Robbert Krebbers committed
59
  the *compatibility lemmas*.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
- [interp.v](exercises/interp.v): The interpretation of syntactic types in terms
Robbert Krebbers's avatar
Robbert Krebbers committed
61
  of semantic types.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
- [fundamental.v](exercises/fundamental.v): The *fundamental theorem*, which
Robbert Krebbers's avatar
Robbert Krebbers committed
63
  states that any syntactically typed program is semantically typed..
Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
- [safety.v](exercises/safety.v): Proofs of semantic and syntactic type safety.
- [unsafe.v](exercises/unsafe.v): Proofs of "unsafe" programs, i.e. programs
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  that are not syntactically typed, but can be proved to be semantically safe.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
- [parametricity.v](exercises/parametricity.v): The use of the semantic typing
Robbert Krebbers's avatar
Robbert Krebbers committed
68
69
70
71
  for proving parametricity results.

Ghost theory for semantic safety of "unsafe" programs:

Robbert Krebbers's avatar
Robbert Krebbers committed
72
- [two_state_ghost.v](exercises/two_state_ghost.v): The ghost theory for a
Robbert Krebbers's avatar
Robbert Krebbers committed
73
  transition system with two states.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
- [symbol_ghost.v](exercises/symbol_ghost.v): The ghost theory for the symbol
Robbert Krebbers's avatar
Robbert Krebbers committed
75
76
77
78
  ADT example.

## Documentation

Robbert Krebbers's avatar
Robbert Krebbers committed
79
The files [proof_mode.md] and [heap_lang.md] in the Iris repository contain a
Robbert Krebbers's avatar
Robbert Krebbers committed
80
81
82
list of the Iris Proof Mode tactics as well as the specialized tactics for
reasoning about HeapLang programs.

Robbert Krebbers's avatar
Robbert Krebbers committed
83
84
[proof_mode.md]: https://gitlab.mpi-sws.org/iris/iris/blob/master/docs/proof_mode.md
[heap_lang.md]: https://gitlab.mpi-sws.org/iris/iris/blob/master/docs/heap_lang.md
Robbert Krebbers's avatar
Robbert Krebbers committed
85
86
87
88
89
90
91
92
93
94
95
96
97

If you would like to know more about Iris, we recommend to take a look at:

- http://iris-project.org/tutorial-material.html
  Lecture Notes on Iris: Higher-Order Concurrent Separation Logic
  Lars Birkedal and Aleš Bizjak
  Used for an MSc course on concurrent separation logic at Aarhus University
- https://www.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf
  Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent
  Separation Logic
  Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars
  Birkedal, Derek Dreyer.
  A detailed description of the Iris logic and its model
98
99
100
101
102
103
104
105
106
107
108

## 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:
```
109
(* SOLUTION *) Proof.
110
  solution here.
111
Qed.
112
113
114
```
is replaced by
```
115
Proof.
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
  (* 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.
```