...
 
Commits (2)
......@@ -17,9 +17,8 @@ Iron has been built and tested with the following dependencies
- 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](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).
2. The fractional authoritative camera described in Section 6 with improper fractions is defined
in [theories/algebra/vfrac_auth.v](theories/algebra/vfrac_auth.v).
- The semantics of the connectives of fractional predicates logic are given in
[theories/bi/fracpred.v](theories/bi/fracpred.v).
......@@ -33,29 +32,29 @@ Iron has been built and tested with the following dependencies
fractional predicates is contained in [theories/proofmode](theories/proofmode).
- In [theories/iron_logic](theories/iron_logic) much of the core Iron logic
discussed in Section 2 is defined.
discussed in Section 3 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
* _Trackable invariants_ as discussed in Section 3.2 are formalized
in [theories/iron_logic/fcinv.v](theories/iron_logic/fcinv.v).
* The definition of weakest preconditions from Section 4 is in
* The definition of weakest preconditions from Section 6 is in
[theories/iron_logic/weakestpre.v](theories/iron_logic/weakestpre.v).
- The formalization specific to the λref,conc is in
[theories/heap_lang](theories/heap_lang).
* The definition of the heap in terms of ghost state from Section 5 is in
* The definition of the heap in terms of ghost state from Section 6 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
* The theorems mentioned in Section 6 about updates to the heap ghost
state are proven in [theories/heap_lang/heap.v](theories/heap_lang/heap.v).
* The state interpretation from Section 5 is defined in
* The state interpretation from Section 6 is defined in
[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
* Theorems 3.1 and 6.1 are proven in
[theories/heap_lang/adequacy.v](theories/heap_lang/adequacy.v).
* The operational semantics from Figure 4 are defined in
* The operational semantics from Figure 5 are defined in
[theories/heap_lang/lang.v](theories/heap_lang/lang.v).
* The rules from Figures 1, 2, 3, and 5 are proven in
* The rules from Figures 4 and 7 are proven in
[theories/heap_lang/lifting.v](theories/heap_lang/lifting.v).
- All of the examples of the paper are formalized and may be found in
......@@ -67,11 +66,11 @@ Iron has been built and tested with the following dependencies
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).
* The example from 4.1 is in [theories/heap_lang/lib/resource_transfer_par.v](theories/heap_lang/lib/resource_transfer_par.v).
* The example from 4.2 is in [theories/heap_lang/lib/resource_transfer_fork.v](theories/heap_lang/lib/resource_transfer_fork.v).
* The example from 4.3 is in [theories/heap_lang/lib/message_passing.v](theories/heap_lang/lib/message_passing.v).
* The example from 4.4 is in [theories/heap_lang/lib/message_passing_example.v](theories/heap_lang/lib/message_passing_example.v).
* The example from 4.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
......