Diaframe is an plugin for Iris trying to improve and expand the automation of proofs.
Diaframe is a plugin for Iris trying to improve and expand the automation of 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).
...
...
@@ -21,8 +21,8 @@ After this you should be able to use `make` to compile the various examples, whi
-`make test`: verifies a spin lock, CLH lock and an ARC
-`make rwlocks`: verifies 4 reader-writer locks in `theories/examples/comparison`
-`make comparison-quick`: verifies 17/24 examples: those which verify relatively quickly.
-`make comparison`: verifies 21/24 examples: verifies 4 additional examples, which take ~3 minute per example. `make comparison` should take about 20-30 minutes on a single core
-`make comparison-all`: verifies all examples. Beware, this takes a while (> 1h on a single core).
-`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).
### Building the examples for external projects (Actris, ReLoC, λ-rust, iris-examples)
...
...
@@ -49,12 +49,12 @@ Although somewhat hard to see directly, these are morally the same.
### Section 4
Important definitions, like (bi-)abduction, can be found in `theories/solve_defs.v`.
The recursive rules for biabduction can be found in `theories/biabd/lemmas.v`.
It takes a bit more work to turn this into a hint-search strategy. This is done in `theories/biabd/search.v`
The recursive rules for biabduction can be found in `theories/hint_search/lemmas_biabd.v`.
It takes a bit more work to turn this into a hint-search strategy. This is done in `theories/hint_search/search_biabd.v`
The biabd-hint-apply rule is shown in `theories/steps/solve_sep.v`. There are two versions of it: a primitive one `solve_sep_biabd`, and a derived one for environments called `tac_solve_sep_ext_biabd`.
The `theories/biabd/instances_base.v` file contains base hints, those that are language-independent. It also contains the Iris-specific hints for invariants. To recursively look inside invariants, there is `inv_into_wand`: an `IntoWand2` instance.
The `theories/hint_search/instances_base.v` file contains base hints, those that are language-independent. Iris-specific hints, like those for invariants, can be found in `theories/lib/iris_hints.v`. To recursively look inside invariants, there is `inv_into_wand`: an `IntoWand2` instance.
This makes the recursive hint see invariants not just as atoms, but also as a wand, for which recursive rules apply.
HeapLang specific hints, like those for `l ↦ v` are located in `theories/heap_lang/biabd_instances_heaplang.v`.
...
...
@@ -97,30 +97,29 @@ These files contain definitions and utilities used throughout the project
-`util_instances.v`: Contains instances of typeclasses defined above
-`env_utils.v`: Contains some additional lemmas for manipulating IPM's environments
-`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/biabd`
#### Files in `theories/hint_search`
These files are all related to the (bi-)abduction hints
-`lemmas.v`: Contains proofs of all recursive rules for constructing bi-abduction hints.
-`lemmas_biabd.v`: Contains proofs of all recursive rules for constructing bi-abduction hints.
-`lemmas_abd.v`: Contains proofs of all recursive rules for constructing abduction hints.
-`search.v`: Defines the search procedure for bi-abduction hints, using the recursive rules.
-`search_biabd.v`: Defines the search procedure for bi-abduction hints, using the recursive rules.
-`search_abd.v`: Defines the search procedure for abduction hints, using the recursive rules.
-`instances_base.v`: Defines the base hint instances, also for Iris.
-`biabd_local_updates.v`: Contains a typeclass based hint derivation procedure for inferring ghost-updates
-`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`
These files contain the proofs and tactics for executing the proof-search strategy.
-`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`: Contains lemmas and tactics for making progress on `Δ ⊢ M (∃ x, A)` goals (`SolveOne` goals). In particular,
contains the proof of the application of abduction hints.
-`introduce_hyp.v`: Contains lemmas and tactis for making progress on `Δ ⊢ H_R -∗ G` goals (`IntroduceHyp` goals). This file is responsible for decomposing `H_R`s into `H_C`s, and for finding interference between hypotheses (i.e. `MergablePersist` or `MergableConsume` instances).
-`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`: Contains lemmas and tactics for making progress on `Δ ⊢ ∀ x. G x` goals (`IntroduceVars` goals). Quite short, no special things happen here.
-`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.
-`drop_modal.v`: Contains some additional typeclass instances used to drop various modalities earlier than above. For example, ensures laters get stripped of timeless assertions when the goal is a fancy update.
-`solve_instances.v`: Contains some additional typeclass instances necessary for using Diaframe's automation.
-`pure_solver.v`: Defines the pure solver used in various places throughout the project.
-`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`: 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`: 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.
The files below are also in this folder, but less relevant:
-`decompose_seps.v`: a tactic for automatically calling `iDestruct` on hypotheses in the context that are separating conjunctions
-`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`: an interface which can be used to provide better names for automatically introduced hypotheses.
#### Files in `theories/symb_exec`
...
...
@@ -136,6 +135,11 @@ This folder defines several ghost-state and hint libraries used in different exa
-`Z_cmra.v`: Instantiates the integers `Z` with addition as a cmra. The `≼` operation is trivial on these
-`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`: 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`: Makes Diaframe strip off the except zero modality when possible when introducing hypotheses. Additionally, makes Diaframe strip off laters of Timeless hypotheses.
-`persistently.v`: Adds support for proving goals behind a `<pers>` modality.
-`intuitionistically.v`: Adds support for proving goals behind a `□` modality.
-`iris_hints.v`: Adds hints specific to Iris's logic - rules for manipulating invariants.
-`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`
Contains all files relevant for instantiating the proof-search strategy for HeapLang
-`class_instances_heaplang.v`: registers the specifications of HeapLangs primitive operations to the proof search strategy.
