RBrlx (RustBelt Relaxed) COQ DEVELOPMENT
This is the Coq development accompanying RBrlx.
Prerequisites
This version is known to compile with:
- Coq 8.8.2 / 8.9.0
- A development version of GPFSL.
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 coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.gitOnce 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.
Building Instructions
Run make -jN to build the full development, where N is the number of your
CPU cores.
Structure
- The folder lang contains the formalization of abstract
specifications for several data structures in the ORC11 relaxed memory
semantics. These data structures are the building blocks for the RBrlx's
version of Rust libraries.
- The repository ORC11 formalizes the operational relaxed memory semantics employed by RBrlx.
- The repository GPFSL formalizes the actual language of RBrlx, as well as the logic for general verification of programs written that language. The language combines ORC11 with an CPS-style expression language (following that of lambda-Rust).
- 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 logic proves the surface-level rules of GPFSL. These rules are the combined version of GPFSL's raw rules with the lifetime logic or the view-dependent invariants.
- 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>.
Where to Find the Proof Rules From the Paper
Type System Rules
The files in typing prove semantic versions of the proof rules given in the original RustBelt 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.
Lifetime Logic Rules
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. The interface of the core lifetime logic is in lifetime_sig.v.
| Proof Rule | File | Lemma |
|---|---|---|
| LftL-begin | model/creation.v | lft_create |
| LftL-tok-fract | model/primitive.v | lft_tok_fractional |
| LftL-tok-fract-obj | model/primitive.v | lft_tok_split_obj |
| LftL-tok-comp | model/primitive.v | lft_tok_sep |
| LftL-tok-unit | model/primitive.v | lft_tok_static |
| LftL-not-own-end | model/primitive.v | lft_tok_dead |
| LftL-end-comp | model/primitive.v | lft_dead_or |
| LftL-end-unit | model/primitive.v | lft_dead_static |
| LftL-borrow | model/borrow.v | bor_create |
| LftL-bor-sep | model/bor_sep.v | bor_sep, bor_combine |
| LftL-bor-fake | model/faking.v | bor_fake |
| LftL-bor-acc-strong | model/accessors.v | bor_acc_strong |
| LftL-bor-acc-atomic-strong | model/accessors.v | bor_acc_atomic_strong |
| LftL-bor-idx | model/primitive.v | bor_unfold_idx |
| LftL-idx-shorten | model/primitive.v | idx_bor_shorten |
| LftL-idx-acc | model/accessors.v | idx_bor_acc |
| LftL-idx-bor-unnest | model/reborrow.v | idx_bor_unnest |
| LftL-idx-bor-iff | model/reborrow.v | idx_bor_iff |
| LftL-bor-in-at | model/in_at_borrow.v | in_at_bor_share |
| LftL-in-at-acc | model/in_at_borrow.v | in_at_bor_acc |
| LftL-in-at-shorten | model/in_at_borrow.v | in_at_bor_shorten |
| LftL-in-at-iff | model/in_at_borrow.v | in_at_bor_iff |
| LftL-incl-isect | model/primitive.v | lft_intersect_incl_l |
| LftL-incl-glb | model/primitive.v | lft_incl_glb |
| LftL-fract-lincl | frac_borrow.v | frac_bor_lft_incl |
| LftL-bor-shorten | lifetime.v | bor_shorten |
| LftL-reborrow | lifetime.v | rebor |
| LftL-bor-unnest | lifetime.v | bor_unnest |
| LftL-bor-acc-cons | lifetime.v | bor_acc_cons |
| LftL-bor-acc | lifetime.v | bor_acc |
| LftL-bor-freeze | lifetime.v | bor_exists |
| LftL-bor-iff | lifetime.v | bor_iff |
| LftL-bor-at | at_borrow.v | at_bor_share |
| LftL-at-acc | at_borrow.v | at_bor_acc |
| LftL-at-shorten | at_borrow.v | at_bor_shorten |
| LftL-at-iff | at_borrow.v | at_bor_iff |
| LftL-bor-na | na_borrow.v | bor_na |
| LftL-na-acc | na_borrow.v | na_bor_acc |
| LftL-na-shorten | na_borrow.v | na_bor_shorten |
| LftL-na-iff | na_borrow.v | na_bor_iff |
| LftL-bor-fracture | frac_borrow.v | bor_fracture' |
| LftL-fract-acc | frac_borrow.v | frac_bor_acc |
| LftL-fract-shorten | frac_borrow.v | frac_bor_shorten |
| LftL-fract-iff | frac_borrow.v | frac_bor_iff |
For Developers: How to update the GPFSL dependency
- Do the change in GPFSL, push it.
- Wait for CI to publish a new Iris version on the opam archive.
- In RBrlx, change opam to depend on the new version.
- Run
make build-dep(in RBrlx) to install the new version of Iris. - You may have to do
make cleanas Coq will likely complain about .vo file mismatches.