tutorial.md

# Tutorial: Verifying a small example using RefinedRust

In this tutorial, we describe how to verify a small example using RefinedRust.
Concretely, we will be verifying a type representing even integers.

To start off, make sure that you have installed the RefinedRust frontend (i.e., that you can run `cargo refinedrust`).
If you used one of our setup scripts or `nix`, this is already the case.
Otherwise, you can perform the following steps in a checkout of this repository:
```
cd rr_frontend
./refinedrust build
./refinedrust install
```

Now, return back to the root of this repository. For simplicity, we are going to locate our new example inside this repository (although you can also locate it elsewhere in your filesystem).

## Getting started

The first step is to create a new Rust project using Cargo.
To that end, perform the following steps:
```
cd case_studies
cargo new evenint
```

This creates a new binary project in the folder `evenint`.
Change to this directory now with `cd evenint`.
You can verify with `cargo run` that the initial auto-generated code runs.

Now, we are going to add in our own code.
To that end, open the file `src/main.rs` in your favorite editor.
Currently, it should contain the following contents:
```
fn main() {
    println!("Hello, world!");
}
```

Let us replace this with the following initial code:

```
fn main() {
    let mut a;
    let b;
    unsafe {
        a = EvenInt::new(0);
        b = EvenInt::new(2);
    }

    a.add_even(&b);
    assert!(a.get() % 2 == 0);
}

struct EvenInt {
    num: i32,
}

impl EvenInt {
    /// Create a new even integer.
    pub unsafe fn new(x: i32) -> Self {
        Self {num: x}
    }

    /// Internal function. Unsafely add 1, making the integer odd.
    unsafe fn add(&mut self) {
        self.num += 1;
    }

    /// Get the even integer
    pub fn get(&self) -> i32 {
        self.num
    }

    /// Add another even integer.
    pub fn add_even(&mut self, other: &Self) {
        self.num += other.num;
    }

    /// Add 2 to an even integer.
    pub fn add_two(&mut self) {
        self.num;

        unsafe {
            self.add();
            self.add();
        }
    }
}
```

Our goal is to verify the assertion in the main function, i.e. that even integers indeed keep up the invariant that they are even.
To do so, we have to verify the interface that `EvenInt` provides by attaching RefinedRust specifications.

## Proving our first function

To get started, we have to tell Rust's compiler to expect RefinedRust annotations.
We can do so by putting the following lines at the top of the file:
```
#![feature(register_tool)]
#![register_tool(rr)]
#![feature(custom_inner_attributes)]
```

Now, the first step is to add an annotation to the struct declaration:
```
#[rr::refined_by("x" : "Z")]
#[rr::invariant("Zeven x")]
struct EvenInt {
    #[rr::field("x")]
    num: i32,
}
```
This invariant says that RefinedRust's mathematical model of `EvenInt` are Coq integers `Z` (using the `refined_by` clause).
The integer should be even, using Coq's `Zeven` predicate.
You can find a more thorough overview in the `SPEC_FORMAT.md` file placed in the same directory as this tutorial.

Using this specification for `EvenInt`, we can already give a sensible specification to the `new` function:
```
#[rr::params("x")]
#[rr::args("x")]
#[rr::requires("Zeven x")]
#[rr::returns("x")]
```

We can run `cargo refinedrust` and `dune build` now, and after short time, the build process should succeed, telling us that the property was successfully verified.

## Inspecting the generated Coq code
Let us now inspect the Coq code that RefinedRust has generated.
By default, RefinedRust will place this code in a subdirectory of Cargo's `target` directory.
To make inspection easier in the sequel, we will configure RefinedRust to put the generated code in an `output` directory in the project directory.
To do so, we create a new file `RefinedRust.toml` in the project directory (alongside `Cargo.toml`) with the following contents:
```
output_dir="./output"
```
You can find more valid configuration options described in RefinedRust's readme.

Now, we can run `cargo clean && cargo refinedrust && dune build` to compile the Coq code in the new directory.

If you inspect the project directory now, you can find a new subdirectory `output` generated by RefinedRust.
Inside `output`, there should be a single directory `evenint` (named after the crate we are verifying), which in turn contains three elements:
* a folder `generated` with code generated by RefinedRust on each invocation of `cargo refinedrust`
* a folder `proofs` with one proof file for each function; these files are only generated on the first invocation and not overwritten on subsequent invocations
* a file `interface.rrlib` that enables RefinedRust to use this crate when verifying another crate using this one.

You can inspect the files `generated/generated_code_evenint.v` to see the Radium definitions RefinedRust generates,
as well as `generated/generated_specs_evenint.v` to see the RefinedRust type definitions generated.
Finally, the `proofs` directory should contain a proof file `proof_EvenInt_new.v` for `EvenInt::new`.

In order to run these files in your favorite Coq editor (e.g. Emacs with ProofGeneral), you need to add the following line to the `_CoqProject` file in the root of the repository:
```
-Q _build/default/case_studies/evenint/output/evenint refinedrust.examples.evenint
```

## Verifying more functions
In the following, we will be verifying the functions `add_two` and `add`.

`add` is slightly interesting because it breaks `EvenInt`'s invariant, since it adds just `1`, making the even integer odd.
Only if called subsequently (as done by `add_two`) can it preserve the invariant.
This is why we have marked `add` as unsafe.

For `add` we take the following specification:
```
#[rr::params("x", "γ")]
#[rr::args(#raw "(#(-[#x]), γ)")]
#[rr::requires("(x + 1 ≤ MaxInt i32)%Z")]
#[rr::observe("γ": "(-[#(x+1)%Z] : plist place_rfn _)")]
```
The first noteworthy part is the `#raw` annotation on the first argument: it asserts that we do not require the invariant on `EvenInt` to currently hold.
That is why we also use `-[#x]` for the contents of the mutable reference, which is the "raw" refinement for the struct (where `x` is the refinement of the first field) without the annotated invariant.
As we add 1, we require that `x + 1` fits into a `i32` integer.

For `add_two`, we add the following specification:
```
#[rr::params("x", "γ")]
#[rr::args("(#x, γ)")]
#[rr::requires("(x + 2 ≤ MaxInt i32)%Z")]
#[rr::observe("γ": "(x+2)")]
```
This works without the `#raw` annotation, as the function keeps the invariant intact.

### Manual proof hints
When checking `add_two`, the RefinedRust solvers will be unable to solve a sidecondition.
Concretely, the proof will fail, with a message of the following shape:
```
Shelved goal remaining in  "EvenInt_add_two" !
Goal:
....
---------
(Inhabited (Zeven (x + 1 + 1)))
```
This message says that RefinedRust's solvers were not able to prove that `x + 1 + 1` is even again!
At this point we have to step in manually.
For that, open the proof file for `EvenInt::add_two`, which should be located at `output/minivec/proofs/proof_EvenInt_add_two.v`.
Currently, it contains mainly a proof of the following shape:
```
Lemma EvenInt_add_two_proof (π : thread_id) :
  EvenInt_add_two_lemma π.
Proof.
  EvenInt_add_two_prelude.

  repeat liRStep; liShow.

  all: print_remaining_goal.
  Unshelve. all: sidecond_solver.
  Unshelve. all: sidecond_hammer.
  Unshelve. all: print_remaining_sidecond.
Qed.
```
This proof will not be overwritten by RefinedRust on subsequent invocations, so we can safely change it.
It consists of the following components:
- `EvenInt_add_two_prelude.` is a function-specific tactic that RefinedRust generated to prepare the proof context.
- `repeat liRStep; liShow.` invokes RefinedRust's type system. After running this, a few shelved pure sideconditions remain.
- the rest of the proof calls into RefinedRust's sidecondition solvers.

In this case, after `sidecond_hammer`, the sidecondition `Zeven (x + 1 + 1)` is still remaining.
Luckily, we know that `Zeven x`, so we can add the following line to solve it:
```
{ rewrite -Z.add_assoc; apply Zeven_plus_Zeven; solve_goal. }
```
The final proof script should look like this:
```
Lemma EvenInt_add_two_proof (π : thread_id) :
  EvenInt_add_two_lemma π.
Proof.
  EvenInt_add_two_prelude.

  repeat liRStep; liShow.

  all: print_remaining_goal.
  Unshelve. all: sidecond_solver.
  Unshelve. all: sidecond_hammer.
  { rewrite -Z.add_assoc; apply Zeven_plus_Zeven; solve_goal. }
  Unshelve. all: print_remaining_sidecond.
Qed.
```

## Your turn!
We leave it as an exercise to the reader to verify the function `add_even`.