README.md 15.1 KB
Newer Older
1
# Diaframe
Ike Mulder's avatar
Ike Mulder committed
2

Ike Mulder's avatar
Ike Mulder committed
3
Diaframe is a plugin for Iris aimed at (partially) automating proofs.
Ike Mulder's avatar
Ike Mulder committed
4

Ike Mulder's avatar
Ike Mulder committed
5
This repository contains the Coq mechanization of Diaframe. The (technical) appendix to Diaframe can be found in the [wiki](https://gitlab.mpi-sws.org/iris/diaframe/-/wikis/Appendix-to-Diaframe).
Ike Mulder's avatar
Ike Mulder committed
6
7
8

## Building the project

Ike Mulder's avatar
Ike Mulder committed
9
Create a new `opam switch` if required (i.e. `opam switch create iris-diaframe 4.10.0`).
Ike Mulder's avatar
Ike Mulder committed
10
11
12
13
14
15
16
17
18
19

Make sure opam can find the Coq and Iris packages:

    opam repo add coq-released https://coq.inria.fr/opam/released
    opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

Install the requirements of this project using

    opam install . --deps-only -j <NUMBEROFJOBS>

Ike Mulder's avatar
Ike Mulder committed
20
21
22
After this you should be able to use `make` to compile the various examples, which are located in [theories/examples/comparison](./theories/examples/comparison):
- `make test`: verifies a spin lock, CLH lock and an ARC.
- `make rwlocks`: verifies the 4 different reader-writer locks.
Ike Mulder's avatar
Ike Mulder committed
23
- `make comparison-quick`: verifies 17/24 examples: those which verify relatively quickly.
Ike Mulder's avatar
Ike Mulder committed
24
25
- `make comparison`: verifies 21/24 examples: verifies 4 additional examples, which take ~2 minute per example. `make comparison` should take about 12-20 minutes on a single core
- `make comparison-all`: verifies all examples. Beware, this takes a while (~40 minutes on a single core).
Ike Mulder's avatar
Ike Mulder committed
26

27
### Building the examples for external projects (Actris, ReLoC, λ-rust, iris-examples)
Ike Mulder's avatar
Ike Mulder committed
28

29
30
31
32
33
First you need to clone the projects in their relevant `external/` folders using

    git submodule update --init --recursive

After this you should be able to use `make` to compile the examples:
Ike Mulder's avatar
Ike Mulder committed
34
- `make actris`: verifies the parallel map implementation provided by Actris, using the automation of this project
35
- `make reloc`: verifies that a ticket lock refines a spin lock, and that a fine-grained stack refines a course-grained stack, using the automation of this project.
Ike Mulder's avatar
Ike Mulder committed
36

Ike Mulder's avatar
Ike Mulder committed
37
38
39
40
41
42
43
44
45
46
47
48
## Overview of tactics
Diaframe provides several tactics to help with proofs.

#### iStepS
The main workhorse of Diaframe. It performs a single *chunk of steps* of the automation described in the paper. What a *chunk of steps* is, depends on the current goal `G`:
- `G = ∀ x, G'`: introduces `x`
- `G = U -∗ G'`: introduces `U`, decomposing it if it is a `∗` or an `∃`. 
- `G = WP e {{ Φ }}` (or any other atom): applies a single abduction hint. For `WP` we have two cases:
  - `e` is a value `v`: new goal is `|={⊤}=> Φ v`
  - `e = K e'` and we can find a specification `SPEC {{ L }} e' {{ U }}`: new goal is `|={⊤}=> L ∗ (∀ v, U -∗ WP (K v) {{ Φ }})`
- `G = |={E1, E2}=> ∃.. x, L ∗ G'`: perform steps of the automation until `L` has been proven, and `G'` remains.
- `G = ⊳ G'`: introduce all laters in the context, continue with goal `G'`.
Ike Mulder's avatar
Ike Mulder committed
49

Ike Mulder's avatar
Ike Mulder committed
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
Note that case 2 and 4 may indeed perform multiple of the steps described in the paper, which is why we say that `iStepS` performs a chunk of steps.

#### iStepsS
`iStepsS` can be thought of as simply `repeat iStepS`. It runs Diaframe's automation until it gets stuck, or no goal remains.

#### iSmash
Sometimes `iStepsS` gets stuck on disjunctions, or goals of the form `|={E1, E2} (L1 ∨ L2) ∗ G`. In this case, you may want to just try if `L1` can be proven, and if not, try `L2`. This is what `iSmash` does: it is basically `iStepsS`, but starts backtracking on choices for the disjunction when it detects a disjunction in the goal.

### Debugging tactics
For debugging purposes, there are two additional tactics.

#### iStepDebug
This puts the goal in a format the automation can understand, but without performing any steps. It prepares the proof state for the next tactic:

#### solveStep
The `solveStep` tactic performs precisely a single step as described in the paper. This can be useful if Diaframe cannot find a hint you thought it would, or finds a different hint. In this case, you can repeat `solveStep` until it differs from your expectation. You can also use `solveStep with <HYPNAME>` to obtain two new goals. The first goal requires you to prove a hint, the second goal is the remaining goal with your hint applied.

67
## Generating the statistics table 
Ike Mulder's avatar
Ike Mulder committed
68
69
70
71
72

Use `python3 -m venv <your_environment_name>` to create a new virtual environment.
Run `pip install tabulate` to install [tabulate](https://pypi.org/project/tabulate/), the table-generation package.
Next, run `python utils/stats_gen.py` from the root of the project. See `python utils/stats_gen.py --help` for more info.

73
74
75
76
77
78
79
80
81
82
83
## Extending or changing Diaframe

If you wish to extend or change Diaframe, this section provides some information to get you started.
- Important definitions can be found in [solve_defs.v](./theories/solve_defs.v) and
[util_classes.v](./theories/util_classes.v). We recommend getting familiar with them before making large changes.
- The rules and corresponding tactics for running the proof automation can all be found in [theories/steps](./theories/steps). There is a file for each relevant goal shape. If you wish to add or change the applied rules, or improve the pure automation, this is the place.
- The rules and procedure for constructing hints recursively can be found in [theories/hint_search](./theories/hint_search). There are separate files for the recursive rules themselves, and the procedure using them. This is not the appropriate folder for adding new base hints!
- If you wish to add a new hint (library), this can be done in [theories/lib](./theories/lib). You can inspect the files in that folder for examples.
- If you wish to add support for a new language, or experiment with changing the support for heap_lang, look at [theories/heap_lang](./theories/heap_lang). This folder contains all files responsible for making Diaframe understand heap_lang verification goals.
- The infrastructure responsible for symbolic execution can be found in [theories/symb_exec](./theories/symb_exec). This is set up quite abstractly, and is capable of handling goals other that WP. Proper documentation of this part is still future work.

84
85
## Directory structure

Ike Mulder's avatar
Ike Mulder committed
86
All Coq files reside in (subdirectories of) the [theories](./theories) folder.
87

Ike Mulder's avatar
Ike Mulder committed
88
#### Files in [theories](./theories)
89
These files contain definitions and utilities used throughout the project
Ike Mulder's avatar
Ike Mulder committed
90
91
92
93
94
- [solve_defs.v](./theories/solve_defs.v): Defines the hint formats `BiAbd` and `Abduct` and the goal formats `SolveSep` and `SolveOne`
- [util_classes.v](./theories/util_classes.v): Defines several typeclasses used throughout the project. An important ones is `ModalityEC`. Roughly speaking, if `ModalityEC M` is true, and we can `SplitModality3 M ?M1 ?M2` the proof-search strategy works behind modality `M`. 
- [util_instances.v](./theories/util_instances.v): Contains instances of typeclasses defined above
- [env_utils.v](./theories/env_utils.v): Contains some additional lemmas for manipulating IPM's environments
- [tele_utils.v](./theories/tele_utils.v): Contains machinery and lemmas to be able to work under existentials, and to be able to separate relevant from irrelevant existentials.
Ike Mulder's avatar
Ike Mulder committed
95

Ike Mulder's avatar
Ike Mulder committed
96
#### Files in [theories/hint_search](./theories/hint_search)
97
These files are all related to the (bi-)abduction hints
Ike Mulder's avatar
Ike Mulder committed
98
99
100
101
102
103
- [lemmas_biabd.v](./theories/hint_search/lemmas_biabd.v): Contains proofs of all recursive rules for constructing bi-abduction hints.
- [lemmas_abd.v](./theories/hint_search/lemmas_abd.v): Contains proofs of all recursive rules for constructing abduction hints.
- [search_biabd.v](./theories/hint_search/search_biabd.v): Defines the search procedure for bi-abduction hints, using the recursive rules.
- [search_abd.v](./theories/hint_search/search_abd.v): Defines the search procedure for abduction hints, using the recursive rules.
- [instances_base.v](./theories/hint_search/instances_base.v): Defines the base hint instances necessary for minimum functionality.
- [explicit_hint_registration.v](./theories/hint_search/explicit_hint_registration.v): Defines a way to reset the registered hints, so the number of distinct hints used can be counted.
Ike Mulder's avatar
Ike Mulder committed
104

Ike Mulder's avatar
Ike Mulder committed
105
#### Files in [theories/steps](./theories/steps)
106
These files contain the proofs and tactics for executing the proof-search strategy.
Ike Mulder's avatar
Ike Mulder committed
107
108
- [solve_sep.v](./theories/steps/solve_sep.v): Contains lemmas and tactics for making progress on `Δ ⊢ || M || ∃ x, A ∗ G` goals (`SolveSep` goals). In particular, contains the proof of the application of bi-abduction hints.
- [solve_one.v](./theories/steps/solve_one.v): Contains lemmas and tactics for making progress on `Δ ⊢  M (∃ x, A)` goals (`SolveOne` goals). In particular,
109
contains the proof of the application of abduction hints.
Ike Mulder's avatar
Ike Mulder committed
110
111
112
113
114
115
116
117
- [introduce_hyp.v](./theories/steps/introduce_hyp.v): Contains lemmas and tactis for making progress on `Δ ⊢ U -∗ G` goals (`IntroduceHyp` goals). This file is responsible for decomposing `U`s into `H_C`s, and for finding interference between hypotheses (i.e. `MergablePersist` or `MergableConsume` instances).
- [introduce_var.v](./theories/steps/introduce_var.v): Contains lemmas and tactics for making progress on `Δ ⊢ ∀ x. G x` goals (`IntroduceVars` goals). Quite short, no special things happen here.
- [merge_mod.v](./theories/steps/merge_mod.v): Contains lemmas and tactics for making progress on `Δ ⊢ ⊳ G` goals (`MergeMod` goals). Works for general `IntroducableModality`s, in practice only used for `⊳`. Responsible for making sure laters get stripped of hypotheses when the goal contains a later.
- [solve_instances.v](./theories/steps/solve_instances.v): Contains some additional typeclass instances necessary for using Diaframe's automation.
- [pure_solver.v](./theories/steps/pure_solver.v): Defines the pure solver used in various places throughout the project.
- [small_steps.v](./theories/steps/small_steps.v): Combines the lemmas and tactics from this folder to construct the `solveSteps` tactic, which runs the proof-search strategy as long as the goals are `SolveSep`, `SolveOne`, `IntroduceHyp`, `IntroduceVars` or `MergeMod`. In this way, it ensures we can run the proof-search strategy to execute a single statement, without observing all tiny steps in between. This is useful for debugging and using the strategy in interactive mode.
- [tactics.v](./theories/steps/tactics.v): Uses the `solveSteps` tactic from `small_steps.v` to build the `iStepS` and `iStepsS` tactics. `iStepS` turns the goal into one of `SolveSep`, `SolveOne`, `IntroduceHyp`, `IntroduceVars` or `MergeMod`, then runs `solveSteps`. `iStepsS` roughly repeatedly calls `iStepS`, and thus runs the proof-search strategy continuously. This file contains some additional instances that make raw `solveStep` goals work better in interactive Iris proofs.
- [verify_tac.v](./theories/steps/verify_tac.v): Uses `iStepsS` to build `verify_tac`. This basically does Löb induction, then runs `iStepsS`. If this stops before finishing, it tries to run `lang_open_tac` to *once* unfold a recursive program. It then runs `iStepsS` again. As we are mainly verifying tail-recursive programs, this strategy works most of the time.
118
119

The files below are also in this folder, but less relevant:
Ike Mulder's avatar
Ike Mulder committed
120
121
- [local_post.v](./theories/steps/local_post.v): a tactic which can be used to add a form of ''proof outlines'' to an Iris proof. Used in the `barrier` and `peterson` example, mainly useful for reducing number of goals to prove if there are a lot of disjunctions.
- [namer_tacs.v](./theories/steps/namer_tacs.v): an interface which can be used to provide better names for automatically introduced hypotheses. 
Ike Mulder's avatar
Ike Mulder committed
122

Ike Mulder's avatar
Ike Mulder committed
123
#### Files in [theories/symb_exec](./theories/symb_exec)
124
This folder contains some infrastructure for generic assertions that can ''execute'', like WP. This is not discussed in the paper. 
Ike Mulder's avatar
Ike Mulder committed
125
126
127
- [defs.v](./theories/symb_exec/defs.v): contains definitions of a generic ''ExecuteOp''.
- [weakestpre.v](./theories/symb_exec/weakestpre.v): contains an instantiation of this for WP.
- [spec_notation.v](./theories/symb_exec/spec_notation.v): defines the `SPEC` notation, in terms of a `ReductionStep` defined in `defs.v`. Comes with an `unfold_spec_goal`, which unfolds a `SPEC` goals into one using just `WP`s.
Ike Mulder's avatar
Ike Mulder committed
128

Ike Mulder's avatar
Ike Mulder committed
129
#### Files in [theories/lib](./theories/lib)
130
This folder defines several ghost-state and hint libraries used in different examples.
Ike Mulder's avatar
Ike Mulder committed
131
132
133
134
135
136
137
138
139
140
141
- [ticket_cmra.v](./theories/lib/ticket_cmra.v): basically a wrapper around the `CoPset` cmra, that separates singletons and the set of all numbers below/under a given one. Used in the `ticket_lock` and the `barrier` examples.
- [frac_token.v](./theories/lib/frac_token.v): Defines the `token`, `no_tokens` and `token_counter` resources from the ARC example. Actually defined on top of:
- [tokenizable.v](./theories/lib/tokenizable.v): More abstract version of above, does not constrain `token`s to only work for Fractionals.
- [Z_cmra.v](./theories/lib/Z_cmra.v): Instantiates the integers `Z` with addition as a cmra. The `≼` operation is trivial on these
- [int_as_nat_diff.v](./theories/lib/int_as_nat_diff.v): It is sometimes useful to represent `Z` as the difference between two (rising) natural numbers. This file extends the pure automation with such a concept. Used in `rwlock_linux_bounded` and the `inc_dec` counter.
- [loc_map.v](./theories/lib/loc_map.v): It is sometimes useful to be able to couple locations to specific data (often `gname`s). This file makes that doable without much hassle.
- [except_zero.v](./theories/lib/except_zero.v): Makes Diaframe strip off the except zero modality when possible when introducing hypotheses. Additionally, makes Diaframe strip off laters of Timeless hypotheses.
- [persistently.v](./theories/lib/persistently.v): Adds support for proving goals behind a `<pers>` modality.
- [intuitionistically.v](./theories/lib/intuitionistically.v): Adds support for proving goals behind a `□` modality.
- [iris_hints.v](./theories/lib/iris_hints.v): Adds hints specific to Iris's logic - rules for manipulating invariants.
- [own_hints.v](./theories/lib/own_hints.v): Adds hints for working with `own γ a` hypotheses, where `a` is a ghost element built from Iris's cmra building blocks (like `auth`, `agree`, `prod`, `option`, `excl`, etcetera.).
Ike Mulder's avatar
Ike Mulder committed
142

Ike Mulder's avatar
Ike Mulder committed
143
#### Files in [theories/heap_lang](./theories/heap_lang)
144
Contains all files relevant for instantiating the proof-search strategy for HeapLang
Ike Mulder's avatar
Ike Mulder committed
145
146
147
- [class_instances_heaplang.v](./theories/heap_lang/class_instances_heaplang.v): registers the specifications of HeapLangs primitive operations to the proof search strategy.
- [biabd_instances_heaplang.v](./theories/heap_lang/biabd_instances_heaplang.v): contains bi-abduction hints for the mapsto-resource, as well as some proof automation to deal with (in)equality of HeapLang values.
- [stepping_tacs.v](./theories/heap_lang/stepping_tacs.v): bundles all required imports for the proof-search strategy instantiated for HeapLang, into one file.
Ike Mulder's avatar
Ike Mulder committed
148

Ike Mulder's avatar
Ike Mulder committed
149
#### Folders in [theories/examples](./theories/examples)
150
Contains 4 folders:
Ike Mulder's avatar
Ike Mulder committed
151
152
153
154
- [comparison](./theories/examples/comparison): Contains the 24 examples discussed in the paper.
- [external](./theories/examples/external): Contains subfolders with examples for lambda-rust, ReLoC, Actris and the iris-examples repository
- [sequential](./theories/examples/sequential): Showcases the proof-search strategy on some classical sequential algorithms
- [wip](./theories/examples/wip): Contains various examples that are still work-in-progress.
Ike Mulder's avatar
Ike Mulder committed
155

Ike Mulder's avatar
Ike Mulder committed
156
#### Files in [theories/legacy](./theories/legacy)
157
Can be ignored, contain old experiments.