Commit 941b9dbd authored by Ike Mulder's avatar Ike Mulder
Browse files


parent 45c1c976
......@@ -40,52 +40,6 @@ Use `python3 -m venv <your_environment_name>` to create a new virtual environmen
Run `pip install tabulate` to install [tabulate](, the table-generation package.
Next, run `python utils/` from the root of the project. See `python utils/ --help` for more info.
## Correspondence to paper
### Section 3
Section 3 culminates in the `sym-ex-fupd-exist` rule. This rule can be found in `theories/symb_exec/weakestpre.v`.
The actual proof search does not apply the lemma as given, but applies the abduction hint `abduct_from_execution`.
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/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/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`.
### Section 5
The `theories/steps` folder contains proofs that all steps in our proof search strategy are sound.
For example `theories/steps/solve_sep.v` contain all steps for the case where our goal is `Δ ⊢ || M || ∃ x, L ∗ G`.
It also contains the the Ltac implementation that automatically applies these steps when applicable, turning our strategy into a usable tactic. For more information on this folder, see Directory Structure.
### Section 6
The `theories/examples/comparison` folders contains the 24 examples from the paper, and possibly some examples that are still work-in-progress.
## Verifying the claims
Diaframe's main claim is that it performs automated and foundational verification of fine-grained concurrent programs.
To check this, we encourage you to:
- Browse the examples in `theories/examples/comparison` to inspect the proof-burden.
- Verify these examples, see 'Building the project'
- Confirm we do not cheat with Axioms. An example file which does this is `theories/examples/comparison/cas_counter_client_closed.v`, which turns the modular specifications of `cas_counter_client` into a closed proof. For more info, see [here](
## Differences between the paper and the Coq development
In the implementation, we always use generic modalities, not fancy updates, in lemmas.
These should be `ModalityEC` modalities: monotone over `⊢`, and satisfy `M P ∗ Q ⊢ M (P ∗ Q)`. Essentially, they are strong functors.
The grammar described in section 5 is *not enforced*. Essentially, the grammar is an informal agreement between Diaframe and its users.
The Coq development contains additional machinery to deal with `⊳` and other modalities, like `⋄`.
The proof search strategy described in section 5 is still a simplified version. WP is actually not necessarily an atom, and applying sym-ex-fupd-exist is not part of the strategy. Instead of sym-ex-fupd-exist, there is an additional type of hints: abduction hints. These are looked for when the goal is just a lone atom. Sym-ex-fupd-exist is 'just' an instance of such an abduction hint.
## Directory structure
All Coq files reside in (subdirectories of) the `theories/` folder.
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