Commit 518525f8 authored by Ike Mulder's avatar Ike Mulder
Browse files

Update README.md

parent f1ba4d22
......@@ -2,11 +2,11 @@
Diaframe is a plugin for Iris aimed at (partially) automating proofs.
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/automation/-/wikis/Appendix-to-Diaframe).
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).
## Building the project
Create a new `opam switch` if required (i.e. `opam switch create iris-automation 4.10.0`).
Create a new `opam switch` if required (i.e. `opam switch create iris-diaframe 4.10.0`).
Make sure opam can find the Coq and Iris packages:
......@@ -34,6 +34,35 @@ After this you should be able to use `make` to compile the examples:
- `make actris`: verifies the parallel map implementation provided by Actris, using the automation of this project
- `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.
## 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'`.
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.
## Generating the statistics table
Use `python3 -m venv <your_environment_name>` to create a new virtual environment.
......@@ -51,6 +80,7 @@ These files contain definitions and utilities used throughout the project
- [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.
#### Files in [theories/hint_search](./theories/hint_search)
These files are all related to the (bi-)abduction hints
- [lemmas_biabd.v](./theories/hint_search/lemmas_biabd.v): Contains proofs of all recursive rules for constructing bi-abduction hints.
......@@ -59,6 +89,7 @@ These files are all related to the (bi-)abduction hints
- [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.
#### Files in [theories/steps](./theories/steps)
These files contain the proofs and tactics for executing the proof-search strategy.
- [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.
......@@ -76,11 +107,13 @@ contains the proof of the application of abduction hints.
The files below are also in this folder, but less relevant:
- [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.
#### Files in [theories/symb_exec](./theories/symb_exec)
This folder contains some infrastructure for generic assertions that can ''execute'', like WP. This is not discussed in the paper.
- [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.
#### Files in [theories/lib](./theories/lib)
This folder defines several ghost-state and hint libraries used in different examples.
- [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.
......@@ -94,16 +127,19 @@ This folder defines several ghost-state and hint libraries used in different exa
- [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.).
#### Files in [theories/heap_lang](./theories/heap_lang)
Contains all files relevant for instantiating the proof-search strategy for HeapLang
- [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.
#### Folders in [theories/examples](./theories/examples)
Contains 4 folders:
- [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.
#### Files in [theories/legacy](./theories/legacy)
Can be ignored, contain old experiments.
Supports Markdown
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