|
| 1 | +# Dust: equality and references support and encoding |
| 2 | + |
| 3 | +Andrea Lattuada, June 2nd 2021 |
| 4 | + |
| 5 | +In the document I will refer to both `struct`s and `enum`s as "algebraic data types", adts in short. For the sake of writing non-contrived examples, we are going to assume that we have chosen a design for "mathematical" sequences that's similar to dafny's sequences. |
| 6 | + |
| 7 | +## Design dimensions |
| 8 | + |
| 9 | +When designing the interface and encoding of equality and reference support for Dust, we need to consider both (a) the user facing language and diagnostics, and (b) the encoding to _z3_ (via _air_). |
| 10 | + |
| 11 | +### Language |
| 12 | + |
| 13 | +Rust uses the `PartialEq` and `Eq` trait to define the `==` (`.eq`) operator for types that implement them. An `==` implementation however does not necessarily conform to structural equality. `Eq` is implemented for `Cell`, but `Cell` has interior mutability (with an unsafe implmentation). |
| 14 | + |
| 15 | +If the programmer uses `#[derive(PartialEq, Eq)]` for an adt without interior mutability, and all the recursively enclosed types have the same property, they obtain an `==` implementation that is structural equality. The built-in `StructuralEq` trait marks those adts where the `==` was automatically derived to be structural equality, but this property is shallow, and does not say anything about whether the enclosed types don't have interior mutability and have structural `==`. |
| 16 | + |
| 17 | +The user needs to know, and sometimes affirm, when a type can be treated as immutable (lacking interior mutability) for the purpose of encoding; additionally, depending on the encoding, it may be important to distinguish between types that have structural equality and those that have an immutable api, but do not have structural equality, like `Vec<int>` (with the exception of `Vec::capacity` and related functions). |
| 18 | + |
| 19 | +We also need to determine whether and how to support verifying the bodies functions for types that have an immutable api but do not have structural equality, e.g. `Vec<int>`. We may decide to restrict this support to the safe interior mutability mechanisms provided by the standard library (`Cell`, `RefCell`, `Mutex`, ...). |
| 20 | + |
| 21 | +### Encoding |
| 22 | + |
| 23 | +#### Adts with structural equality |
| 24 | + |
| 25 | +Adts that only contain primitive types (possibly by means of other adts with the same property) can always have an equality implementation that conforms to smt equality (with structural equality). These can be encoded as _air_ datatypes, like in the following example: |
| 26 | + |
| 27 | +```rust |
| 28 | +#[derive(PartialEq, Eq)] |
| 29 | +struct Thing { a: int, b: bool } |
| 30 | +... |
| 31 | +let t = Thing { a: 12, b: true }; |
| 32 | +``` |
| 33 | + |
| 34 | +``` |
| 35 | +(declare-datatypes () ((Thing (Thing/Thing (Thing/Thing/a Int) (Thing/Thing/b Bool))))) |
| 36 | +... |
| 37 | +(declare-const t@ Thing) |
| 38 | +(assume |
| 39 | + (= t@ (Thing/Thing 12 true)) |
| 40 | +) |
| 41 | +``` |
| 42 | + |
| 43 | +For these types, if the `==` implementation is structural equality, we can encode `==` to smt equality: |
| 44 | + |
| 45 | +```rust |
| 46 | +affirm(Thing { a: 12, b: true } != Thing { a: 14, b: true }); |
| 47 | +``` |
| 48 | + |
| 49 | +``` |
| 50 | +(assert |
| 51 | + "<span>" (req%affirm (not (= (Thing/Thing 12 true) (Thing/Thing 14 true))))) |
| 52 | +``` |
| 53 | + |
| 54 | +This encoding is however unsound in general for any other adt, for example, for the following struct: |
| 55 | + |
| 56 | +```rust |
| 57 | +#[derive(Eq)] |
| 58 | +struct Custom { a: int } |
| 59 | + |
| 60 | +impl std::cmp::PartialEq for Custom { |
| 61 | + fn eq(&self, other: &Self) -> bool { |
| 62 | + self.a == other.a + 1 |
| 63 | + } |
| 64 | +} |
| 65 | +``` |
| 66 | + |
| 67 | +This also extends to generic adts whenever the type parameters also have equality that conforms to smt equality (with structural equality). |
| 68 | + |
| 69 | +```rust |
| 70 | +#[derive(PartialEq, Eq)] |
| 71 | +struct Foo<A> { a: A, b: bool } |
| 72 | +``` |
| 73 | + |
| 74 | +In this example `==` of `Foo<Thing>` would conform to smt equality, but `Foo<Custom>` would not. |
| 75 | + |
| 76 | +#### Adts that have interior mutability (and/or raw pointers) but expose an "immutable" interface |
| 77 | + |
| 78 | +This set of types can also be defined those adts that do _not_ have well-defined structural equality (i.e. where at least one of the fields has interior mutability, is a raw pointer, or is another adt that recursively contains these) but "hide" the interior mutability in their public interface, and act like "immutable" types. |
| 79 | + |
| 80 | +`RefCell` is not one such type, as one can change its value while holding a shared reference. The following is such a (slightly contrived) type: |
| 81 | + |
| 82 | +```rust |
| 83 | +struct List { |
| 84 | + contents: RefCell<Box<[u64]>>, |
| 85 | +} |
| 86 | + |
| 87 | +impl List { |
| 88 | + /// Makes an empty List |
| 89 | + pub fn new() -> List { |
| 90 | + List { contents: RefCell::new(Box::new()) } |
| 91 | + } |
| 92 | + |
| 93 | + /// Push an item at the end of the list |
| 94 | + pub fn push(&mut self, v: u64) { |
| 95 | + let borrowed = self.contents.borrow_mut(); |
| 96 | + // use borrowed to reallocate the boxed slice, and copy data over |
| 97 | + } |
| 98 | + |
| 99 | + /// Get the item at position i, or None if it doesn't exist |
| 100 | + pub fn get(&self, i: usize) -> Option<u64> { |
| 101 | + self.contents.borrow().get(i) |
| 102 | + } |
| 103 | +} |
| 104 | +``` |
| 105 | + |
| 106 | +Again, we treat generic adts as having this property if the type parameters have at least structural equality. The design needs to clarify whether there's a difference between "immutable" adts with generic arguments that have structural equality and those with generic arguments that are themselves "immutable" adts. |
| 107 | + |
| 108 | +Possibly with the exception of `Vec::capacity` and related methods, `Vec<T>` is a type that satisfies this property, when `T` is either structural (`Vec<Thing>`) or "immutable" (`Vec<Vec<Thing>>`). |
| 109 | + |
| 110 | +## Using _traits_ to strengthen a function's or type's spec |
| 111 | + |
| 112 | +The rust standard library sometimes uses ("marker") traits to denote that a certain type has a specific property, potentially that a certain function has a stronger (more restrictive) specification. One example is `stc::cmp::Eq`: this trait does not define any new functions, but types implementing it promise that the `PartialEq::eq` (`==`) implementation is an equivalence relation: in addition to it being symmetric and transitive (as required by `PartialEq`), `Eq` asserts that `==` is also reflexive. Another example is `std::marker::Send` and `std::marker::Sync`, which asserts that a type is can be safely transferred across thread boundaries, and that it's one for which it's safe to share references across threads, respectively. |
| 113 | + |
| 114 | +As described in the following section(s), we plan on leaning on this to extend the specification for `==` to, e.g., structural equality, for the types that conform to it. |
| 115 | + |
| 116 | +## The `builtin::Structural` trait, and visibility |
| 117 | + |
| 118 | +Because the `std::marker::StructuralEq` reflects only shallow structural equality, we add a verifier-specific marker trait, `builtin::Structural`, which can only be implemented for an adt if its `==` implementation conforms to structural equality. Adts that implement this trait are encoded as `air` datatypes, and `==` for these types is encoded as smt equality, whenever all of their fields are visible in the current scope; if at least _one_ of the fields is not visible, the encoding will be opaque, as discussed later. |
| 119 | + |
| 120 | +The `trait builtint::Structural` can be implemented by the user, and the verifier checks that the type can indeed recursively conform to structural equality, and that the `==` implementation matches. If there are type parameters, these must also restricted to implement `builtin::Structural`. A `derive` macro is provided, so that the user can write: |
| 121 | + |
| 122 | +```rust |
| 123 | +#[derive(PartialEq, Eq, Structural)] |
| 124 | +struct Thing<T> { |
| 125 | + value: T, |
| 126 | +} |
| 127 | +``` |
| 128 | + |
| 129 | +The following derived `Structural` implementation would match the following: |
| 130 | + |
| 131 | +```rust |
| 132 | +impl<T: builtin::Structural> builtin::Structural for Thing<T> { } |
| 133 | +``` |
| 134 | + |
| 135 | +## `builtin::Structural` types with non-visible fields |
| 136 | + |
| 137 | +When referencing a `Structural` type from a separate module where some of the fields are not visible (not `pub`/ `pub(crate)`), we encode the entire type as an opaque z3 "sort". |
| 138 | + |
| 139 | +## `builtin::Immutable`, `builtin::ImmutableEq` for adts that (may) have interior mutability (and/or raw pointers) but expose an "immutable" interface |
| 140 | + |
| 141 | +When a type may have interior mutability, but exposes an "immutable" interface (through its entire API), the user can mark it `Immutable`. Additionally, the trait `builtin::ImmutableEq` asserts that `==` conforms to "mathematical" (smt) equality. `Immutable` is required for `ImmutableEq`. |
| 142 | + |
| 143 | + |
| 144 | + |
| 145 | +--- |
| 146 | + |
| 147 | + |
| 148 | + |
| 149 | +## The `builtin::View` trait, and `builtin::ViewEq` |
| 150 | + |
| 151 | +In general, specifications for public functions of a type should be written in terms of an abstract representation of the type's contents. A `Vec<u64>` should be represented just as a sequence (maybe, a slice) of integers; by default none of the facts necessary to prove the implementation should leak into the publicly visible specification of the interface. In our experience with _Veribetrfs_, inadvertently exposing internal invariants and properties is one of the common causes of long verification times and timeouts; this is because the solver has access to facts internal to the implementations that are irrelevant but can still be selected and cause qunatifier triggers to fire. |
| 152 | + |
| 153 | +With the exception of very simple ADTs that have all public fields and implement `Structural`, the abstract representation of a type must be specified by implementing the `View` trait: |
| 154 | + |
| 155 | +```rust |
| 156 | +trait View { |
| 157 | + type View : std::marker::StructEq; |
| 158 | + |
| 159 | + #[spec] |
| 160 | + fn view(&self) -> Self::View { unimplemented!() } |
| 161 | +} |
| 162 | +``` |
| 163 | + |
| 164 | +So, for `Vec`, we'd implement `View` as something like: |
| 165 | + |
| 166 | +```rust |
| 167 | +impl<T: builtin::StructEq> builtin::View for Vec<T> { |
| 168 | + type View = [T]; // (a sequence of T's) |
| 169 | +} |
| 170 | +``` |
| 171 | + |
| 172 | +The specification for `Vec::push` and `Vec::get` can then be along the lines of: |
| 173 | + |
| 174 | +```rust |
| 175 | +pub fn push(&mut self, value: T) { |
| 176 | + ensures(self.view() == old(self).view() + [value]); |
| 177 | +``` |
| 178 | + |
| 179 | +```rust |
| 180 | +pub fn get(&self, index: usize) -> Option<T> { |
| 181 | + ensures(result == self.view()[index]); |
| 182 | +``` |
| 183 | + |
| 184 | +Note that we did not provide an implementation for the `view` function. Generally speaking, `.view()` is unaffected by functions on the type that take immutable references. We are still working out the details on when `.view()` should be havoc'd. |
| 185 | + |
| 186 | +The `builtin::ViewEq` trait indicates that the equality implemented by `==` matches view equality, which is always structural equality of the `View`. `builtin::ViewEq` is an `unsafe` trait, as the verifier generally cannot check whether `==` matches view equality. There are two ways of imlpementing `ViewEq`: |
| 187 | + |
| 188 | +1. The user can manually write `unsafe impl builtin::ViewEq for T`, and this becomes part of the TCB. The `unsafe` keyword allows easy inspection. |
| 189 | +2. The user can use a derive macro to `#[derive(ViewEq)]` the implementation for a type that also implements `View`. In this case the verifier will check that `a == b` $ \Leftrightarrow $ `a.view() == b.view()`. |
| 190 | + |
| 191 | +Implementing `View` also requires that the view does **not** change except for when we have `mut` or `&mut T`: to start this is trivially enforced by having `View` require `Immutable` or `Structural`. |
| 192 | + |
| 193 | +## Immutable references, `&_ T` |
| 194 | + |
| 195 | + |
| 196 | + |
| 197 | +Control havoc-ing with the `builtin::Immutable` trait. `StructEq` implies `Immutable` and `View` requires `Immutable`? |
| 198 | + |
| 199 | + |
| 200 | + |
| 201 | +## TODO |
| 202 | + |
| 203 | +* [ ] When to havoc `.view()` |
| 204 | +* [ ] What about `Vec<T>` where `T` is "immutable" |
| 205 | +* [ ] What about `Vec<T>` where `T` has interior mutability -- punt on this? |
| 206 | +* [ ] `Hash` |
| 207 | +* [x] Auto-`opaque` |
| 208 | + |
0 commit comments