# RMRM (RustBelt Meets Relaxed Memory) COQ DEVELOPMENT
This is the Coq development accompanying lambda-Rust.
This is the Coq development accompanying RMRM.
## Prerequisites
This version is known to compile with:
- Coq 8.7.2 / 8.8.0
- A development version of [GPFSL](https://gitlab.mpi-sws.org/FP/gpfsl/)
- 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:
...
...
@@ -31,14 +31,15 @@ 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 [lang](theories/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 RMRM's version of Rust libraries.
* The repository [ORC11] formalizes the operational relaxed memory semantics employed by RMRM.
* The repository [GPFSL] formalizes the actual language of RMRM, 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](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 [logic](theories/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](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.
...
...
@@ -93,7 +94,7 @@ borrows" in the Coq development.
| 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.
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](theories/typing/examples) subfolder.
### Lifetime Logic Rules
...
...
@@ -125,11 +126,14 @@ then sealed behind a module signature in
| 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
## For Developers: How to update the GPFSL dependency
* Do the change in Iris, push it.
* Do the change in [GPFSL], push it.
* 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.
* In RMRM, change opam to depend on the new version.
* Run `make build-dep` (in RMRM) to install the new version of Iris.
* You may have to do `make clean` as Coq will likely complain about .vo file
