@@ -4,21 +4,13 @@ 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 and examples can be found in the `rr_frontend` 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.
### For the `rr_frontend` subfolder:
### Structure of the generated code:
For each input module `mod`, the RefinedRust generates the following files in the corresponding output directory:
*`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.
*`extra_proofs_mod.v` allows users to add custom theory for use in specifications and proofs.
* for each function `fun` with annotated specifications: a file `generated_proof_fun.v` containing the automatically-generated typing proof that calls into RefinedRust's automation.
* the `rust_typing` subfolder contains the implementation of the RefinedRust type system and proof automation.
## Setup
### Setup instructions for the Coq code:
...
...
@@ -42,32 +34,50 @@ make builddep
```
3. Build the project
```
dune build
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
To use RefinedRust's frontend to generate the Coq input for RefinedRust's type system, switch to the `rr-frontend` directory.
Then, assuming you want to translate `path-to-file.rs`, run:
```
./refinedrust run -- path-to-file.rs
```
For example:
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:
```
./refinedrust run -- examples/paper.rs
cd case_studies/paper-examples
cargo refinedrust
dune build
```
This will create a new directory called `paper` in the `output` folder.
To then compile the generated Coq code, switch to `output/paper` and run `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.
@@ -9,7 +9,7 @@ As an example, the following function has specifications attached to it that say
```rust
#[rr::params(z)]
#[rr::args("z")]
#[rr::requires("⌜z + 42 ∈ i32⌝")]
#[rr::requires("z + 42 ∈ i32")]
#[rr::returns("z + 42")]
fnadd_42(x:i32)->i32{
x+42
...
...
@@ -22,9 +22,9 @@ RefinedRust infers a "default" type for the argument from Rust's type, but this
For instance, the clause `#[rr::args("z" @ "int i32")]` would be equivalent to the one specified above.
In addition, for types (like structs) with invariants declared on them, the argument can be prefixed with `#raw` in order to not require the invariant on them to hold (e.g. `#[rr::args("z", #raw "-[#x]")]`).
The `requires` clause specifies the requirement that the result of the addition fits into an `i32`. This can in general include arbitrary Iris propositions.
Arbitrary Coq propositions (like `z+42 ∈ i32`) can be embedded into Iris by wrapping it with `⌜`/`⌝` brackets.
Finally, the returns clause specifies a refinement (and optionally, a type) for the return value of the function.
The `requires` clause specifies the requirement that the result of the addition fits into an `i32` (see [RefinedRust propositions](#refinedrust-propositions) for details on the syntax).
Finally, the `returns` clause specifies a refinement (and optionally, a type) for the return value of the function.
| Keyword | Purpose | Properties | Example |
...
...
@@ -33,8 +33,8 @@ Finally, the returns clause specifies a refinement (and optionally, a type) for
| `exists` | specify an existential for the postcondition | multiple | `#[rr::exists("x" : "Z")]` |
There are further attributes that influence the proof-checking behaviour:
...
...
@@ -90,6 +90,20 @@ Inside a crate, the following crate-level attributes can be specified:
-`#![rr::coq_prefix("A.B.C")]`: puts the generated files under the logical Coq path `A.B.C`
-`#![rr::import("A.B.C", "D")]`: imports the file `D` from logical Coq path `A.B.C` in all spec and proof files
## RefinedRust propositions
For propositional specifications, as appearing in `#[rr::requires("P")]`, `#[rr::ensures("P")]`, and `#[rr::invariant("P")]`, specific notational shortcuts are supported.
By default, `P` is interpreted as a (pure) Coq proposition (i.e., it is interpreted to the Iris proposition `⌜P⌝`).
This can be changed by format specifiers starting with `#` which preceed the string `"P"`:
- The `#iris` format specifier interprets `P` as an Iris proposition.
- Type assignments for locations/places can be specified by the `#type "l" : "r" @ "ty"` template, specifying that `l` is an owned pointer storing a value of type `r @ ty`.
- In `rr::invariant` clauses on structs, the `#own` specifier only makes the following Iris proposition available in the invariant for owned types.
- In `rr::invariant` clauses on structs, the `#shr` specifier only makes the following Iris proposition available in the invariant for shared types.
In the default interpretation as pure Coq propositions, optionally a name can be specified that will be used in Coq's context (if the proposition becomes a hypothesis), by writing (for instance) `#[rr::requires("Hx" : "x < 5")]`.
This is especially useful for semi-manual proofs.
## Special syntax
### Escape sequences
As a rule of thumb, all string literals in specifications are inserted literally into the generated Coq code.
...
...
@@ -108,19 +122,6 @@ In particular, we support the following escape sequences:
To prevent an expression wrapped in curly braces to be transformed, write two curly braces: `{{ ... }}`.
This will be replaced by `{ ... }`.
## RefinedRust propositions
For propositional specifications, as appearing in `#[rr::requires("P")]`, `#[rr::ensures("P")]`, and `#[rr::invariant("P")]`, specific notational shortcuts are supported.
By default, `P` is interpreted as a (pure) Coq proposition (i.e., it is interpreted to the Iris proposition `⌜P⌝`).
This can be changed by format specifiers starting with `#` which preceed the string `"P"`:
- The `#iris` format specifier interprets `P` as an Iris proposition.
- Type assignments for locations/places can be specified by the `#type "l" : "r" @ "ty"` template, specifying that `l` is an owned pointer storing a value of type `r @ ty`.
- In `rr::invariant` clauses on structs, the `#own` specifier only makes the following Iris proposition available in the invariant for owned types.
- In `rr::invariant` clauses on structs, the `#shr` specifier only makes the following Iris proposition available in the invariant for shared types.
In the default interpretation as pure Coq propositions, optionally a name can be specified that will be used in Coq's context (if the proposition becomes a hypothesis), by writing (for instance) `#[rr::requires("Hx" : "x < 5")]`.
