ravencheck 0.5.0

Decidable verification of Rust code using relational abstraction.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101

# `ravencheck`

`ravencheck` is a tool for symbolic verification of Rust code, using guaranteed-decidable SMT queries for predictable results.

## Usage

First, make sure you have the [CVC5](https://cvc5.github.io/) SMT
solver available. You should be able to run `cvc5 --version` in your
dev environment.

Then, add `ravencheck` as a dependency in your Cargo.toml file, using
one of these three methods:

### Depend on crates.io package

Add the following to your Cargo.toml:

```
[dependencies]
ravencheck = "0.5.0"
```

This gives you the latest published version (v0.5.0).

### Depend on the GitHub repo's latest commit

Add the following to your Cargo.toml:

```
[dependencies]
ravencheck = { git = "https://github.com/cuplv/ravencheck" }
```

This gives you the latest commit to `main`.

### Depend on local copy of the repo

Alternatively, you can clone the repo and use its path on your
filesystem as the dependency:

```
# Cargo.toml
...
[dependencies]
ravencheck = { path = "path/to/cloned/repo" }
...
```

This allows you to choose which commit in the repo to use.

### Verifying a module

You use `ravencheck` by adding the `#[ravencheck::check_module]` macro
attribute at the top of modules in which you want to use
verification. 

```
#[ravencheck::check_module]
#[declare_types(u32)]
mod rvn {
    #[declare]
    const ZERO: u32 = 0;

    #[declare]
    fn le(a: u32, b: u32) -> bool {
        a <= b
    }

    #[assume]
    fn le_anti_symmetric() -> bool {
        forall(|x: u32, y: u32| {
            implies(
                le(x,y) && le(y,x),
                x == y
            )
        })
    }

    #[assume]
    fn zero_is_least() -> bool {
        forall(|x: u32| le(ZERO, x))
    }

    #[verify]
    fn prop1(x: u32) -> bool {
        implies(
            le(x, ZERO),
            x == ZERO
        )
    }
}
```

See the [crate documentation](https://docs.rs/ravencheck/latest/ravencheck/) for more details, as well as the `examples/` directory in this repo.

## About

"Raven" is an acronym for *relationally-abstracted verification
encoding*, the technique that is used to reduce verification
conditions to a decidable fragment of first-order logic (specifically,
the Extended EPR fragment).