Newer
Older
## Prerequisites
This version is known to compile with:
- A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
The easiest way to install the correct versions of the dependencies is through
opam (1.2.2 or newer). You will need the Coq and Iris opam repositories:
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies.
## Updating
After doing `git pull`, the development may fail to compile because of outdated
dependencies. To fix that, please run `opam update` followed by `make
build-dep`.
Run `make -jN` to build the full development, where `N` is the number of your
CPU cores.
## Structure
* The folder [lang](theories/lang) contains the formalization of the lambda-Rust
core language, including the theorem showing that programs with data races get
stuck.
* The folder [lifetime](theories/lifetime) proves the rules of the lifetime
logic, including derived constructions like (non-)atomic persistent borrows.
* The subfolder [model](theories/lifetime/model) proves the core rules, which
are then sealed behind a module signature in
[lifetime.v](theories/lifetime/lifetime.v).
* The folder [typing](theories/typing) defines the domain of semantic types,
interpretations of all the judgments, as well as proofs of all typing rules.
* [type.v](theories/typing/type.v) contains the definition of a semantic type.
* [programs.v](theories/typing/programs.v) defines the typing judgements for
instructions and function bodies.
* [soundness.v](theories/typing/soundness.v) contains the main soundness
theorem of the type system.
* The subfolder [examples](theories/typing/examples) shows how the examples
from the technical appendix can be type-checked in Coq.
* The subfolder [lib](theories/typing/lib) contains proofs of safety of some
unsafely implement types from the Rust standard library and some user
crates: `Cell`, `RefCell`, `Rc`, `Arc`, `Mutex`, `RwLock`, `mem::swap`,
`thread::spawn`, `take_mut::take`, `alias::once` as well as converting `&&T`
to `&Box<T>`.
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
## Where to Find the Proof Rules From the Paper
### Type System Rules
The files in [typing](theories/typing) prove semantic versions of the proof
rules given in the paper. Notice that mutable borrows are called "unique
borrows" in the Coq development.
| Proof Rule | File | Lemma |
|-----------------------|-----------------|-----------------------|
| T-bor-lft (for shr) | shr_bor.v | shr_mono |
| T-bor-lft (for mut) | uniq_bor.v | uniq_mono |
| C-subtype | type_context.v | subtype_tctx_incl |
| C-copy | type_context.v | copy_tctx_incl |
| C-split-bor (for shr) | product_split.v | tctx_split_shr_prod2 |
| C-split-bor (for mut) | product_split.v | tctx_split_uniq_prod2 |
| C-share | borrow.v | tctx_share |
| C-borrow | borrow.v | tctx_borrow |
| C-reborrow | uniq_bor.v | tctx_reborrow_uniq |
| Tread-own-copy | own.v | read_own_copy |
| Tread-own-move | own.v | read_own_move |
| Tread-bor (for shr) | shr_bor.v | read_shr |
| Tread-bor (for mut) | uniq_bor.v | read_uniq |
| Twrite-own | own.v | write_own |
| Twrite-bor | uniq_bor.v | write_uniq |
| S-num | int.v | type_int_instr |
| S-nat-leq | int.v | type_le_instr |
| S-new | own.v | type_new_instr |
| S-delete | own.v | type_delete_instr |
| S-deref | programs.v | type_deref_instr |
| S-assign | programs.v | type_assign_instr |
| F-consequence | programs.v | typed_body_mono |
| F-let | programs.v | type_let' |
| F-letcont | cont.v | type_cont |
| F-jump | cont.v | type_jump |
| F-newlft | programs.v | type_newlft |
| F-endlft | programs.v | type_endlft |
| F-call | function.v | type_call' |
Some of these lemmas are called `something'` because the version without the `'` is a derived, more speicalized form used together with our eauto-based `solve_typing` tactic. You can see this tactic in action in the [examples](theories/typing/examples) subfolder.
### Lifetime Logic Rules
The files in [lifetime](theories/lifetime) prove the lifetime logic, with the
core rules being proven in the [model](theories/lifetime/model) subfolder and
then sealed behind a module signature in
[lifetime.v](theories/lifetime/lifetime.v).
| Proof Rule | File | Lemma |
|-------------------|---------------------|----------------------|
| LftL-begin | model/creation.v | lft_create |
| LftL-tok-fract | model/primitive.v | lft_tok_fractional |
| LftL-not-own-end | model/primitive.v | lft_tok_dead |
| LftL-end-persist | model/definitions.v | lft_dead_persistent |
| LftL-borrow | model/borrow.v | bor_create |
| LftL-bor-split | model/bor_sep.v | bor_sep |
| LftL-bor-acc | lifetime.v | bor_acc |
| LftL-bor-shorten | model/primitive.v | bor_shorten |
| LftL-incl-isect | model/primitive.v | lft_intersect_incl_l |
| LftL-incl-glb | model/primitive.v | lft_incl_glb |
| LftL-tok-inter | model/primitive.v | lft_tok_sep |
| LftL-end-inter | model/primitive.v | lft_dead_or |
| LftL-tok-unit | model/primitive.v | lft_tok_static |
| LftL-end-unit | model/primitive.v | lft_dead_static |
| LftL-reborrow | lifetime.v | rebor |
| LftL-bor-fracture | frac_borrow.v | bor_fracture |
| LftL-fract-acc | frac_borrow.v | frac_bor_atomic_acc |
| LftL-bor-na | na_borrow.v | bor_na |
| LftL-na-acc | na_borrow.v | na_bor_acc |
## For Developers: How to update the Iris dependency
* Wait for CI to publish a new Iris version on the opam archive.
* In lambdaRust, change opam to depend on the new version.
* Run `make build-dep` (in lambdaRust) to install the new version of Iris.
* You may have to do `make clean` as Coq will likely complain about .vo file