LAMBDA-RUST COQ DEVELOPMENT

This is the Coq development accompanying lambda-Rust.

Prerequisites

This version is known to compile with:

• Coq 8.6
• Ssreflect 1.6.1
• A development version of Iris

The easiest way to install the correct versions of the dependencies is through opam. Coq packages are available on the coq-released repository, set up by the command:

opam repo add coq-released https://coq.inria.fr/opam/released

Once you got opam set up, just run make build-dep to install the right versions of the dependencies. When the dependencies change, just run make build-dep again.

Building Instructions

Run make to build the full development.

Structure

• 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 folder typing defines the domain of semantic types, interpretations of all the judgments, as well as proofs of all typing rules.
  • 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::once as well as converting &&T to &Box<T>.

For Developers: How to update the Iris dependency

• Do the change in Iris, push it.
• In lambdaRust, change opam.pins to point to the new commit.
• 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 mismatches.