Tweak README.

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`