From 1a34a493fa8dbd99915606c80c4aed5f283cd507 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Wed, 31 Oct 2018 20:55:08 +0100 Subject: [PATCH] Tweak README. --- README.md | 193 +++++++++++++++++++++++++++--------------------------- 1 file changed, 96 insertions(+), 97 deletions(-) diff --git a/README.md b/README.md index 7ae20d2..d129179 100644 --- a/README.md +++ b/README.md @@ -14,69 +14,68 @@ Iron has been built and tested with the following dependencies ## Directory Structure -- In `theories/algebra` two new cameras are defined. +- In [theories/algebra](theories/algebra) two new cameras are defined. 1. Improper fractions as a camera without identity with addition as - the operation are defined in `theories/algebra/vfrac.v`. + the operation are defined in [theories/algebra/vfrac.v](theories/algebra/vfrac.v). 2. The fractional authoritative camera described in Section 5 built with improper fractions is defined in - `theories/algebra/vfrac_auth.v`. + [theories/algebra/vfrac_auth.v](theories/algebra/vfrac_auth.v). -- The semantics of the connectives of the lifted logic are given in - `theories/bi/fracpred.v`. +- The semantics of the connectives of fractional predicates logic are given in + [theories/bi/fracpred.v](theories/bi/fracpred.v). This file does not contain a description of the lifted program logic but instead contains the definitions of ∧, ∗, ∀, and other the other connectives. It also contains all the rules of the specific to this logic that are used later. -- The machinery for connecting the generalized proofmode from - `iris-coq` to fractional predicates is contained in - `theories/proofmode`. +- The machinery for connecting the generalized proofmode/MoSeL from to + fractional predicates is contained in (theories/proofmode)[theories/proofmode]. -- In `theories/iron_logic` much of the core Iron logic discussed - in Section 2 is defined. - * Uniformity with respect to fractions is defined in - `theories/iron_logic/iron.v` as `Uniform` and +- In (theories/iron_logic)[theories/iron_logic] much of the core Iron logic + discussed in Section 2 is defined. + * _Uniformity_ with respect to fractions is defined in + [theories/iron_logic/iron.v](theories/iron_logic/iron.v) as `Uniform` and several closure properties of it are proved. - * Trackable invariants as discussed in Section 2.1 are formalized - in `theories/iron_logic/fcinv.v`. + * _Trackable invariants_ as discussed in Section 2.1 are formalized + in [theories/iron_logic/fcinv.v](theories/iron_logic/fcinv.v). * The definition of weakest preconditions from Section 4 is in - `theories/iron_logic/weakestpre.v`. + [theories/iron_logic/weakestpre.v](theories/iron_logic/weakestpre.v). - The formalization specific to the λref,conc is in - `theories/heap_lang`. - * The definition of the heap in terms of ghost state from Section - 5 is in `theories/heap_lang/heap.v` as `heapG`. So too are - the definitions of ↦ and e (in the formalization called `perm`). + [theories/heap_lang](theories/heap_lang). + * The definition of the heap in terms of ghost state from Section 5 is in + [theories/heap_lang/heap.v](theories/heap_lang/heap.v) as `heapG`. So too + are the definitions of ↦ and 𝖊 (in the formalization called `perm`). * The theorems stated in Section 5 about updates to the heap ghost - state are proven in `theories/heap_lang/heap.v`. + state are proven in (theories/heap_lang/heap.v)[theories/heap_lang/heap.v]. * The state interpretation from Section 5 is defined in - `theories/heap_lang/heap.v` as `heap_ctx`. + [theories/heap_lang/heap.v](theories/heap_lang/heap.v) as `heap_ctx`. * Theorems 2.1, 2.2, 4.1, and 4.2 are proven in - `theories/heap_lang/adequacy.v`. + [theories/heap_lang/adequacy.v](theories/heap_lang/adequacy.v). * The operational semantics from Figure 4 are defined in - `theories/heap_lang/lang.v`. + [theories/heap_lang/lang.v](theories/heap_lang/lang.v). * The rules from Figures 1, 2, 3, and 5 are proven in - `theories/heap_lang/lifting.v`. + [theories/heap_lang/lifting.v](theories/heap_lang/lifting.v). - All of the examples of the paper are formalized and may be found in - `theories/heap_lang/lib/`. All of the examples are formalized - purely within the lifted logic. There is no fraction accounting in + [theories/heap_lang/lib/](theories/heap_lang/lib/). All of the examples are + formalized purely within the lifted logic. There is no fraction accounting in the proofs and no significant bookkeeping beyond what is found in vanilla Iris. - As mentioned in the paper, a small portion of `par` cannot be - formalized in the lifted logic but in the formalization this is - factored out into `spawn` in `theories/heap_lang/lib/spawn.v`. - * The example from 3.1 is in `theories/heap_lang/lib/resource_transfer_par.v`. - * The example from 3.2 is in `theories/heap_lang/lib/resource_transfer_fork.v`. - * The example from 3.3 is in `theories/heap_lang/lib/message_passing.v`. - * The example from 3.4 is in `theories/heap_lang/lib/message_passing_example.v`. - * The example from 3.5 is in `theories/heap_lang/lib/par.v`. + As mentioned in the paper, a small portion of `par` cannot be formalized in + the lifted logic but in the formalization this is factored out into `spawn` + in [theories/heap_lang/lib/spawn.v](theories/heap_lang/lib/spawn.v) + * The example from 3.1 is in [theories/heap_lang/lib/resource_transfer_par.v](theories/heap_lang/lib/resource_transfer_par.v). + * The example from 3.2 is in [theories/heap_lang/lib/resource_transfer_fork.v](theories/heap_lang/lib/resource_transfer_fork.v). + * The example from 3.3 is in [theories/heap_lang/lib/message_passing.v](theories/heap_lang/lib/message_passing.v). + * The example from 3.4 is in [theories/heap_lang/lib/message_passing_example.v](theories/heap_lang/lib/message_passing_example.v). + * The example from 3.5 is in [theories/heap_lang/lib/par.v](theories/heap_lang/lib/resource_transfer_par.v). Note that `spawn.v`, `resource_transfer_par.v`, and `resource_transfer_fork.v` use the same state transition system (from Figure 3). This is formalized in - `theories/heap_lang/lib/transfer_resource_sts.v`. + [theories/heap_lang/lib/transfer_resource_sts.v](theories/heap_lang/lib/transfer_resource_sts.v). ## Differences Between the Formalization and The Paper @@ -152,9 +151,9 @@ This can be used to derive `LINV-ALLOC` when used in conjunction with There is a correspondence between the invariant rules presented in the paper with Hoare triples and those in the formalization. - - `TINV-ALLOC` and `LTINV-ALLOC` follow from `fcinv_alloc_named`. - - `TINV-OPEN` and `LTINV-OPEN` follow from `fcinv_open`. - - `TINV-DEALLOC` and `LTINV-DEALLOC` follow from `fcinv_cancel`. +- `TINV-ALLOC` and `LTINV-ALLOC` follow from `fcinv_alloc_named`. +- `TINV-OPEN` and `LTINV-OPEN` follow from `fcinv_open`. +- `TINV-DEALLOC` and `LTINV-DEALLOC` follow from `fcinv_cancel`. All of these theorems are proven in `theories/iron_logic/fcinv.v`. @@ -172,63 +171,63 @@ The format of the table is as follows: Name of Theorem/Rule/Definition/Proposition, the name in the formalization, and the file in the formalization. - - The language definition in Section 2, `expr`, `theories/heap_lang/lang.v` - - `e` and `↦`, `perm` and `↦`, `theories/heap_lang/heap.v` - - Trackable invariants, `fcinv`, `theories/iron_logic/fcinv.v` - - `OPerm(-, -)`, `fcinv_own`, `theories/iron_logic/fcinv.v` - - `DPerm(-, -)`, `fcinv_cancel_own`, `theories/iron_logic/fcinv.v` - - `HOARE-FRAME`, `hoare_frame_r`, `iris-coq/theories/program_logic/hoare.v` - - `HOARE-VAL`, `ht_val`, `iris-coq/theories/program_logic/hoare.v` - - `HOARE-λ`, `pure_rec`, `theories/heap_lang/lifting.v` - - `HOARE-BIND`, `ht_bind`, `iris-coq/theories/program_logic/hoare.v` - - `EMP-SPLIT`, `perm_split`, `theories/heap_lang/heap.v` - - `PT-SPLIT`, `mapsto_uniform`, `theories/heap_lang/heap.v` - - `PT-DISJ`, `mapsto_valid_2`, `theories/heap_lang/heap.v` - - `HOARE-ALLOC`, `wp_alloc`, `theories/heap_lang/lifting.v` - - `HOARE-FREE`, `wp_free`, `theories/heap_lang/lifting.v` - - `HOARE-LOAD`, `wp_load`, `theories/heap_lang/lifting.v` - - `HOARE-STORE`, `wp_store`, `theories/heap_lang/lifting.v` - - `HOARE-FORK-EMP`/`HOARE-FORK-TRUE`, `wp_fork`, `theories/heap_lang/lifting.v` - - `INV-DUP`, `inv_persistent`, `theories/heap_lang/lifting.v` - - `INV-ALLOC`, `inv_alloc`, `iris-coq/theories/base_logic/lib/invariants.v` - - `INV-OPEN`, `inv_open`, `iris-coq/theories/base_logic/lib/invariants.v` - - `TINV-SPLIT`, `fcinv_own_fractional`, `theories/iron_logic/fcinv.v` - - `TINV-DUP`, `fcinv_persistent`, `theories/iron_logic/fcinv.v` - - `TINV-ALLOC`, `fcinv_alloc_named`, `theories/iron_logic/fcinv.v` - - `TINV-OPEN`, `fcinv_open`, `theories/iron_logic/fcinv.v` - - `TINV-DEALLOC`, `fcinv_cancel`, `theories/iron_logic/fcinv.v` - - Uniform with respect to fractions, `Uniform`, `theories/iron_logic/iron.v` - - `HOARE-CONS`, `ht_vs`, `iris-coq/theories/program_logic/hoare.v` - - The rules from Figure 4, `head_step`, `theories/heap_lang/lang.v` - - Theorem 2.1, `heap_adequacy`, `theories/heap_lang/adequacy.v` - - Theorem 2.2, `heap_strong_adequacy`, `theories/heap_lang/adequacy.v` - - `HOARE-PAR`, `par_spec`, `theories/heap_lang/lib/par.v` - - The example from 3.1, `transfer_works1`, `theories/heap_lang/lib/resource_tranfer_par.v` - - The example from 3.2, `transfer_works1`, `theories/heap_lang/lib/resource_tranfer_fork.v` - - The example from 3.3, Several theorems, `theories/heap_lang/lib/message_passing.v` - - The example from 3.4, `program_spec`, `theories/heap_lang/lib/message_passing_example.v` - - The example from 3.5, Several theorems, `theories/heap_lang/lib/{spawn, par}.v` - - Definitions of lifted connectives, Several definitions, `theories/bi/fracpred.v` - - Definition of lifted `↦`, `↦`, `theories/heap_lang/heap.v` - - `LHOARE-FRAME`, `iron_wp_frame_r`, `iris-coq/theories/program_logic/hoare.v` - - `LHOARE-VAL`, `iron_wp_val`, `iris-coq/theories/program_logic/hoare.v` - - `LHOARE-λ`, `pure_rec`, `theories/heap_lang/lifting.v` - - `LHOARE-BIND`, `iron_wp_bind`, `iris-coq/theories/program_logic/hoare.v` - - `LPT-DISJ`, `mapsto_valid_2`, `theories/heap_lang/heap.v` - - `LHOARE-ALLOC`, `iron_wp_alloc`, `theories/heap_lang/lifting.v` - - `LHOARE-FREE`, `iron_wp_free`, `theories/heap_lang/lifting.v` - - `LHOARE-LOAD`, `iron_wp_load`, `theories/heap_lang/lifting.v` - - `LHOARE-STORE`, `iron_wp_store`, `theories/heap_lang/lifting.v` - - `LHOARE-FORK`, `iron_wp_fork`, `theories/heap_lang/lifting.v` - - `LTINV-SPLIT`, `fcinv_own_fractional`, `theories/iron_logic/fcinv.v` - - `LTINV-DUP`, `fcinv_persistent`, `theories/iron_logic/fcinv.v` - - `LTINV-ALLOC`, `fcinv_alloc_named`, `theories/iron_logic/fcinv.v` - - `LTINV-OPEN`, `fcinv_open`, `theories/iron_logic/fcinv.v` - - `LTINV-DEALLOC`, `fcinv_cancel`, `theories/iron_logic/fcinv.v` - - Definition of Hoare triples, `iron_wp`, `theories/iron_logic/weakestpre.v` - - Theorem 4.1, `heap_adequacy`, `theories/heap_lang/adequacy.v` - - Theorem 4.2, `heap_strong_adequacy`, `theories/heap_lang/adequacy.v` - - Definition of WP in Section 5, `wp_def`, `iris-coq/theories/program_logic/weakestpre.v` - - Definition of state interp from Section 5, `heap_ctx`, `theories/heap_lang/heap.v` - - Theorem 5.1, `wp_strong_all_adequacy`, `iris-coq/theories/program_logic/adequacy.v` +- The language definition in Section 2, `expr`, `theories/heap_lang/lang.v` +- `e` and `↦`, `perm` and `↦`, `theories/heap_lang/heap.v` +- Trackable invariants, `fcinv`, `theories/iron_logic/fcinv.v` +- `OPerm(-, -)`, `fcinv_own`, `theories/iron_logic/fcinv.v` +- `DPerm(-, -)`, `fcinv_cancel_own`, `theories/iron_logic/fcinv.v` +- `HOARE-FRAME`, `hoare_frame_r`, `iris-coq/theories/program_logic/hoare.v` +- `HOARE-VAL`, `ht_val`, `iris-coq/theories/program_logic/hoare.v` +- `HOARE-λ`, `pure_rec`, `theories/heap_lang/lifting.v` +- `HOARE-BIND`, `ht_bind`, `iris-coq/theories/program_logic/hoare.v` +- `EMP-SPLIT`, `perm_split`, `theories/heap_lang/heap.v` +- `PT-SPLIT`, `mapsto_uniform`, `theories/heap_lang/heap.v` +- `PT-DISJ`, `mapsto_valid_2`, `theories/heap_lang/heap.v` +- `HOARE-ALLOC`, `wp_alloc`, `theories/heap_lang/lifting.v` +- `HOARE-FREE`, `wp_free`, `theories/heap_lang/lifting.v` +- `HOARE-LOAD`, `wp_load`, `theories/heap_lang/lifting.v` +- `HOARE-STORE`, `wp_store`, `theories/heap_lang/lifting.v` +- `HOARE-FORK-EMP`/`HOARE-FORK-TRUE`, `wp_fork`, `theories/heap_lang/lifting.v` +- `INV-DUP`, `inv_persistent`, `theories/heap_lang/lifting.v` +- `INV-ALLOC`, `inv_alloc`, `iris-coq/theories/base_logic/lib/invariants.v` +- `INV-OPEN`, `inv_open`, `iris-coq/theories/base_logic/lib/invariants.v` +- `TINV-SPLIT`, `fcinv_own_fractional`, `theories/iron_logic/fcinv.v` +- `TINV-DUP`, `fcinv_persistent`, `theories/iron_logic/fcinv.v` +- `TINV-ALLOC`, `fcinv_alloc_named`, `theories/iron_logic/fcinv.v` +- `TINV-OPEN`, `fcinv_open`, `theories/iron_logic/fcinv.v` +- `TINV-DEALLOC`, `fcinv_cancel`, `theories/iron_logic/fcinv.v` +- Uniform with respect to fractions, `Uniform`, `theories/iron_logic/iron.v` +- `HOARE-CONS`, `ht_vs`, `iris-coq/theories/program_logic/hoare.v` +- The rules from Figure 4, `head_step`, `theories/heap_lang/lang.v` +- Theorem 2.1, `heap_adequacy`, `theories/heap_lang/adequacy.v` +- Theorem 2.2, `heap_strong_adequacy`, `theories/heap_lang/adequacy.v` +- `HOARE-PAR`, `par_spec`, `theories/heap_lang/lib/par.v` +- The example from 3.1, `transfer_works1`, `theories/heap_lang/lib/resource_tranfer_par.v` +- The example from 3.2, `transfer_works1`, `theories/heap_lang/lib/resource_tranfer_fork.v` +- The example from 3.3, Several theorems, `theories/heap_lang/lib/message_passing.v` +- The example from 3.4, `program_spec`, `theories/heap_lang/lib/message_passing_example.v` +- The example from 3.5, Several theorems, `theories/heap_lang/lib/{spawn, par}.v` +- Definitions of lifted connectives, Several definitions, `theories/bi/fracpred.v` +- Definition of lifted `↦`, `↦`, `theories/heap_lang/heap.v` +- `LHOARE-FRAME`, `iron_wp_frame_r`, `iris-coq/theories/program_logic/hoare.v` +- `LHOARE-VAL`, `iron_wp_val`, `iris-coq/theories/program_logic/hoare.v` +- `LHOARE-λ`, `pure_rec`, `theories/heap_lang/lifting.v` +- `LHOARE-BIND`, `iron_wp_bind`, `iris-coq/theories/program_logic/hoare.v` +- `LPT-DISJ`, `mapsto_valid_2`, `theories/heap_lang/heap.v` +- `LHOARE-ALLOC`, `iron_wp_alloc`, `theories/heap_lang/lifting.v` +- `LHOARE-FREE`, `iron_wp_free`, `theories/heap_lang/lifting.v` +- `LHOARE-LOAD`, `iron_wp_load`, `theories/heap_lang/lifting.v` +- `LHOARE-STORE`, `iron_wp_store`, `theories/heap_lang/lifting.v` +- `LHOARE-FORK`, `iron_wp_fork`, `theories/heap_lang/lifting.v` +- `LTINV-SPLIT`, `fcinv_own_fractional`, `theories/iron_logic/fcinv.v` +- `LTINV-DUP`, `fcinv_persistent`, `theories/iron_logic/fcinv.v` +- `LTINV-ALLOC`, `fcinv_alloc_named`, `theories/iron_logic/fcinv.v` +- `LTINV-OPEN`, `fcinv_open`, `theories/iron_logic/fcinv.v` +- `LTINV-DEALLOC`, `fcinv_cancel`, `theories/iron_logic/fcinv.v` +- Definition of Hoare triples, `iron_wp`, `theories/iron_logic/weakestpre.v` +- Theorem 4.1, `heap_adequacy`, `theories/heap_lang/adequacy.v` +- Theorem 4.2, `heap_strong_adequacy`, `theories/heap_lang/adequacy.v` +- Definition of WP in Section 5, `wp_def`, `iris-coq/theories/program_logic/weakestpre.v` +- Definition of state interp from Section 5, `heap_ctx`, `theories/heap_lang/heap.v` +- Theorem 5.1, `wp_strong_all_adequacy`, `iris-coq/theories/program_logic/adequacy.v` -- GitLab