RefinedRust verification framework

This repository contains a public mirror of the RefinedRust development version.

Structure

The Coq implementation of RefinedRust can be found in the theories subfolder. The frontend implementation can be found in the rr_frontend subfolder. Case studies and tests can be found in the case_studies subfolder. Stdlib interfaces (without proofs) can be found in the stdlib subfolder.

For the theories subfolder:

• the caesium subfolder contains the Radium operational semantics, an adaptation of RefinedC's Caesium semantics.
• the lithium subfolder contains RefinedC's Lithium separation logic automation engine with very lightweight modifications.
• the rust_typing subfolder contains the implementation of the RefinedRust type system and proof automation.

Setup

Setup instructions for the Coq code:

We assume that you have opam installed on your system. Setup instructions can be found here: https://opam.ocaml.org/doc/Install.html

0. cd into the directory containing this README.

1. Create a new opam switch for RefinedRust:

opam switch create refinedrust --packages=ocaml-variants.4.14.0+options,ocaml-option-flambda
opam switch link refinedrust .
opam switch refinedrust
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

2. Install the necessary dependencies:

opam pin add coq 8.17.1
opam pin add coq-lambda-rust.dev https://gitlab.mpi-sws.org/lgaeher/lambda-rust.git#rr
make builddep

3. Build the project

dune build theories

Setup instructions for the frontend:

1. Make sure that you have a working rustup/Rust install. Instructions for setting up Rust can be found on https://rustup.rs/.
2. Run ./refinedrust build in rr_frontend to build the frontend.
3. Run ./refinedrust install in rr_frontend to install the frontend.

The last command will install RefinedRust's frontend into Rustup's install directory.

Frontend usage

After installing RefinedRust, it can be invoked through cargo, Rust's build system and package manager, by running cargo refinedrust.

For example, you can build the examples from the paper (located in case_studies/paper-examples) by running:

cd case_studies/paper-examples
cargo refinedrust
dune build

The invocation of cargo refinedrust will generate a folder output/paper_examples with two subdirectories: generated and proofs. The generated subdirectory contains auto-generated code that may be overwritten by RefinedRust at any time during subsequent invocations. The proofs subdirectory contains proofs which may be edited manually (see the section Proof Editing below) and are not overwritten by RefinedRust.

More specifically, the generated directory will contain:

• generated_code_crate.v contains the definition of the code translated to the Radium semantics, including layout specifications for the used structs and enums.
• generated_specs_crate.v contains the definition of the annotated specifications for functions and data structures in terms of RefinedRust's type system.
• for each function fun with annotated specifications: a file generated_template_fun.v containing the lemma statement that has to be proven to show the specification, as well as auto-generated parts of the proof that may change when implementation details of fun are changed.

The proofs subdirectory contains for each function fun a proof that invokes the components defined in the generated_template_fun.v file.

In addition, RefinedRust generates an interface.rrlib file containing the ADTs and functions which are publicly exported and specified. Verification of other crates can import these specifications. The lib_load_paths config option influences where the verifier searches for these interface files. The crate-level rr::include directive can be used to import these proof files (see the description in SPEC_FORMAT.md).

Proof editing

In order to interactively look at the generated code using a Coq plugin like Coqtail, VSCoq, or Proof General for the editor of your choice, you need to add a line pointing to the directory of the generated code in the _CoqProject file. See the existing includes for inspiration.

Changes to the proof_*.v files in the generated proofs folder are persistent and files are not changed once RefinedRust has generated them once. This enables to write semi-automatic proofs. proof_*.v files are intended to be checked into git, as they are stable.

On changes to implementations or specifications, only the files located in generated are modified. The default automatic proofs in proof_*.v files are stable under any changes to a function. Of course, once you change proofs manually, changing an implementation or specification may require changes to your manually-written code.

Frontend Configuration

Configuration options can be set in the RefinedRust.toml file. These include:

The path to the config file can also be specified via the environment variable RR_CONFIG. Setting this variable will also change the work_dir (relative to which paths are interpreted) to the path of RR_CONFIG.

Overrides for all settings can be specified in the environment via variables with the prefix RR_, e.g. RR_SHIMS, RR_DUMP_BORROWCK_INFO, etc.

License

We currently re-use code from the following projects:

• rustc: https://github.com/rust-lang/rust (under the MIT license)
• miri: https://github.com/rust-lang/miri (under the MIT license)
• RefinedC: https://gitlab.mpi-sws.org/iris/refinedc (under the BSD 3-clause license)
• Iris: https://gitlab.mpi-sws.org/iris/iris (under the BSD 3-clause license)
• lambda-rust: https://gitlab.mpi-sws.org/iris/lambda-rust (under the BSD 3-clause license)
• Prusti: https://github.com/viperproject/prusti-dev (under the MPL 2.0 license)
• Coq ident-to-string: https://github.com/mit-plv/coqutil/blob/master/src/coqutil/Macros/ident_to_string.v (under the MIT license)

We provide the RefinedRust code under the BSD 3-clause license.