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
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155

Here is an overview of how SMT queries are formed from `#[verify]`
conditions.

# Original query

```
fn add_twice(a: Nat, b: Nat) -> Nat {
    if b == Nat::Z {
        a
    } else {
        add(add(a, b), b)
    }
}

#[verify]
fn add_twice_monotonic() -> bool {
    !exists(|x: Nat, y: Nat| {
        gt(x, add_twice(x,y))
    })
}
```

# 1. Convert to CBPV

Ravencheck's internal representation
is Call-By-Push-Value style.
The conversion from surface-level Rust sytnax
is implemented in `lang/src/rir/from_syn.rs`.

The converted query example here
is written out using Rust syntax,
but internally Ravencheck uses the AST 
defined in `lang/src/rir/ast.rs`
to represent the code.
The AST is defined by the mutually-inductive
`Comp` and `Val` enum types.

```
fn add_twice(a: Nat, b: Nat) -> Nat {
    let v0 = b == Nat::Z;
    if v0 {
        return a
    } else {
        let v1 = add(a, b);
        let v2 = add(v1, b);
        return v2
    }
}

#[verify]
fn add_twice_monotonic() -> bool {
    let v3 = exists(|x: Nat, y: Nat| {
        let v4 = add_twice(x,y);
        let v5 = gt(x, v4);
        return v5
    });
    let v6 = !v3;
    return v6
}
```

# 2. Partial evaluaion

In this step, queries are evaluated as much as possible,
leaving only symbolic values and functions.
In this example, the `add_twice` function 
is eliminated by inlining.
In contrast, calls 
to the primitive/uninterpreted `add` function 
remain.

This is performed 
by functions in `lang/src/partial_eval.rs`.

The result is still represented
using the `Comp`/`Val` AST.

```
#[verify]
fn add_twice_monotonic() -> bool {
    let v3 = exists(|x: Nat, y: Nat| {
        let v0 = y == Nat::Z;
        if v0 {
            let v5 = gt(x, x);
            return v5
        } else {
            let v1 = add(x, y);
            let v2 = add(v1, y);
            let v5 = gt(x, v2);
            return v2
        }
    });
    let v6 = !v3;
    return v6
}
```

# 3. Negation-normal-form

Performed by `lang/src/neg_normal_form.rs`.

```
#[verify]
fn add_twice_monotonic() -> bool {
    forall(|x: Nat, y: Nat| {
        let v0 = y == Nat::Z;
        if v0 {
            let v5 = !gt(x, x);
            return v5
        } else {
            let v1 = add(x, y);
            let v2 = add(v1, y);
            let v5 = !gt(x, v2);
            return v5
        }
    });
}
```

# 4. Relational abstraction

Performed by `lang/src/expand_funs.rs`.

```
#[verify]
fn add_twice_monotonic() -> bool {
    forall(|x: Nat, y: Nat| {
        let v0 = y == Nat::Z;
        if v0 {
            let v5 = !gt(x, x);
            return v5
        } else {
            forall(|v1: Nat| implies(
                add_ra(x, y, v1),
                forall(|v2: Nat| implies(
                    add_ra(v1, y, v2),
                    {
                        let v5 = !gt(x, v2);
                        return v5
                    }
                ))
            ))
        }
    })
}
```

# 5. Conversion to SMT

Performed by `lang/src/smt/internal.rs`.

This takes the `Comp`/`Val` AST
and produces an `easy-smt` AST,
which is then converted by the `easy-smt` package
into actual SMTLIB code and fed to CVC5.