This is the Coq development accompanying lambda-Rust.
This version is known to compile with:
- Coq 8.15.1
- A development version of Iris
When building from source, we recommend to use opam (2.0.0 or newer) for installing the dependencies. This requires the following two repositories:
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
Once you got opam set up, run make build-dep to install the right versions
of the dependencies.
Run make -jN to build the full development, where N is the number of your
CPU cores.
To update, do git pull. After an update, the development may fail to compile
because of outdated dependencies. To fix that, please run opam update
followed by make build-dep.
- The folder lang contains the formalization of the lambda-Rust core language, including the theorem showing that programs with data races get stuck.
- The folder lifetime proves the rules of the lifetime
logic, including derived constructions like (non-)atomic persistent borrows.
- The subfolder model proves the core rules, which are then sealed behind a module signature in lifetime.v.
- The folder typing defines the domain of semantic types,
interpretations of all the judgments, as well as proofs of all typing rules.
- type.v contains the definition of a semantic type.
- programs.v defines the typing judgements for instructions and function bodies.
- soundness.v contains the main soundness theorem of the type system.
- The subfolder examples shows how the examples from the technical appendix can be type-checked in Coq.
- The subfolder 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::onceas well as converting&&Tto&Box<T>.
In this section we list fundamental changes to the model that were done since the publication of the original RustBelt paper.
As part of the GhostCell paper, the model was adjusted to support branding.
- The semantic interpretation of external lifetime contexts had to be changed to use a syntactic form of lifetime inclusion.
- This changed interpretation broke the proof of "lifetime equalization". Instead we prove a weaker rule that only substitutes lifetimes on positions that are compatible with semantic lifetime inclusion. This is good enough for the example.
- Furthermore, we had to redo the proof of
type_call_iris', a key lemma involved in calling functions and ensuring that their assumptions about lifetime parameters do indeed hold. The old proof exploited semantic lifetime inclusion in external lifetime contexts in a crucial step. The proof was fixed by adjusting the semantic interpretation of the local lifetime context. In particular there is a new parameterqmaxhere that has to be threaded through everywhere.
The files in 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 specialized form used together with our eauto-based solve_typing tactic. You can see this tactic in action in the examples subfolder.
The files in lifetime prove the lifetime logic, with the core rules being proven in the model subfolder and then sealed behind a module signature in 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 |
- Do the change in Iris, push it.
- Wait for CI to publish a new Iris version on the opam archive, then run
opam update iris-dev. - In lambdaRust, change the
opamfile to depend on the new version. - Run
make build-dep(in lambdaRust) to install the new version of Iris. You may have to domake cleanas Coq will likely complain about .vo file mismatches.