# 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.

### 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](#proof-editing) below) and are not overwritten by RefinedRust.

More specifically, the `generated` directory will contain for each crate `mod`:
* `generated_code_mod.v` contains the definition of the code translated to the Radium semantics, including layout specifications for the used structs and enums.
* `generated_specs_mod.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.

## 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:

| Option | Type | Configures |
|--------|------|------------|
| `work_dir` | Relative/absolue path | Determines the working directory. Other relative paths are interpreted relative to this one. |
| `dump_borrowck_info` | Boolean | Dumps borrowck debug output in the log directory |
| `output_dir` | Relative/absolute path | Determines the directory where the generated output files will be placed |
| `log_dir` | Relative/absolute path | Determines the directory where logs and debug dumps will be placed if enabled |
| `shims` | Relative path | Determines the JSON file storing information about shims that RefinedRust uses |
| `run_check` | Boolean | Automatically call the Coq type checker on the generated files |
| `verify_deps` | Boolean | Verify dependencies or not |
| `admit_proofs` | Boolean | Skip Coq's `Qed` check and instead run `Admitted` |

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.