invariant-reference 0.1.0

Helps code authors define and use invariants
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

# Intro

When writing Rust code that contains `.expect()` calls, we need to provide a message that explains
why the panic is impossible here, e.g.:

```rust
fn main() {
    let items = make_items();
    let first = items.get(0).expect("`items` is initialized to 3 items");
}

fn make_items() -> Vec<i32> {
    vec![1, 2, 3]
}
```

The use of string message for `.expect()` is not ideal, as its contents is not checked by the compiler,
and it is hard to provide a compact message with a comprehensive explanation.

We can make some important observations:
- the `.expect()` call is actually a use of some invariant
- some other place in code must ensure that this invariant holds.

E.g., for the example code:
- the invariant is "`make_items` returns a non-empty vector"
- this invariant is ensured in the body of `make_items` function
- this invariant is used in the body of `main` function

This library aims to improve this by providing at least some of degree of compiler checking for `.expect()` calls.
We let the Rust's type system to check that all used references are proven in some other place of code.

With the help of `invariant_reference`, the example code is written as:
```rust
fn main() {
    let items = make_items();
    let first = items.get(0).unwrap_under_invariant::<MakeItemsReturnsNonEmpty>();
}

#[derive(Invariant)]
#[invariant(message = "make_items() returns non-empty vector")]
struct MakeItemsReturnsNonEmpty;

fn make_items() -> Vec<i32> {
    invariant_established!(MakeItemsReturnsNonEmpty, why = "vec with 3 items is non-empty");
    vec![1, 2, 3]
}
```

This style of code has several advantages:
- the invariants are explicitly defined in code
- the developer is force to provide some explanation of what the invariant means and why it is upheld
- the `invariant_established!` is placed close to the code that ensures that the invariant holds;
  during code review it is easier to spot mistakes in such code
- we can use "Find All References" function to find all places that depend on an invariant

# How to use

1. Add references to `invariant_reference` and `invariant_reference_derive` crates
2. Define the invariant as a struct with the `#[derive(Invariant)]` macro:
   ```
   #[derive(Invariant)]
   #[invariant(message = "the xyz vector is not empty", num_proofs = 1)]
   struct XyzVecIsNotEmpty;
   ```
   - provide the `message` that explains the essence of the invariant, i.e. what condition must hold true
   - optionally, if an invariant is established in multiple places (e.g., a struct has multiple constructors),
     specify the number of such code paths in the `num_proofs` attribute.
3. Invoke the `invariant_established!(XyzVecIsNotEmpty, why = "...")` macro in the specific code place where it makes sense
   (e.g., in the body of a struct constructor)
   - use `invariant_established!(XyzVecIsNotEmpty[0], why = "...")` macro if there are multiple such places
4. Invoke `OptionExt::unwrap_under_invariant::<XyzVecIsNotEmpty>()` or `ResultExt::unwrap_under_invariant::<XyzVecIsNotEmpty>()` instead of `.expect()`

# Notes and limitations

- The code will fail to compile if `invariant_established!` is not invoked (even if the invariant is not referenced) or invoked multiple times for the same invariant (unless using different indices)
- `invariant_established!` may only be called within the same crate, as this libraries relies on traits.