Add documentation for traits (#2537)

Author: parno

examples/guide/traits.rs

@@ -0,0 +1,186 @@
+// rust_verify/tests/example.rs expect-success
+use vstd::prelude::*;
+
+verus! {
+
+// ANCHOR: basic_trait
+trait Compressor {
+    fn compress(&self, input: u64) -> (output: u64)
+        ensures output <= input;
+}
+// ANCHOR_END: basic_trait
+
+// ANCHOR: impl_extends
+struct HalfCompressor;
+
+impl Compressor for HalfCompressor {
+    // The trait's `ensures output <= input` is automatically inherited.
+    // We additionally specify the exact return value.
+    fn compress(&self, input: u64) -> (output: u64)
+        ensures output == input / 2,
+    {
+        input / 2
+    }
+}
+// ANCHOR_END: impl_extends
+
+// ANCHOR: dispatch
+fn compress_generic<C: Compressor>(c: &C, x: u64) {
+    let r = c.compress(x);
+    assert(r <= x); // OK: trait-level ensures holds for every C
+}
+
+fn compress_concrete(c: &HalfCompressor, x: u64) {
+    let r = c.compress(x);
+    assert(r <= x);      // From the trait ensures
+    assert(r == x / 2);  // From HalfCompressor's stronger ensures (statically resolved)
+}
+// ANCHOR_END: dispatch
+
+// ANCHOR: requires_ensures
+trait Bounded {
+    fn clamp(&self, val: u64, lo: u64, hi: u64) -> (result: u64)
+        requires lo <= hi,
+        ensures lo <= result <= hi;
+}
+// ANCHOR_END: requires_ensures
+
+// ANCHOR: requires_ensures_impl
+struct Saturate;
+
+impl Bounded for Saturate {
+    // Inherits: requires lo <= hi, ensures lo <= result <= hi
+    // Adds: the exact formula for result
+    fn clamp(&self, val: u64, lo: u64, hi: u64) -> (result: u64)
+        ensures result == if val < lo { lo } else if val > hi { hi } else { val },
+    {
+        if val < lo { lo } else if val > hi { hi } else { val }
+    }
+}
+// ANCHOR_END: requires_ensures_impl
+
+// ANCHOR: spec_trait
+trait Distance {
+    spec fn dist(&self, other: &Self) -> nat;
+
+    fn distance(&self, other: &Self) -> (d: u64)
+        ensures
+            d as nat == self.dist(other),
+    ;
+
+    proof fn valid_distance_metric()
+        ensures
+            forall |x: &Self, y| x.dist(y) == y.dist(x),
+            forall |x: &Self, y| x.dist(y) == 0 <==> x == y,
+            forall |x: &Self, y, z| x.dist(y) <= x.dist(z) + z.dist(y),
+        ;
+}
+// ANCHOR_END: spec_trait
+
+// ANCHOR: spec_trait_impl
+struct P {
+    u: u64
+}
+
+impl Distance for P {
+    spec fn dist(&self, other: &Self) -> nat {
+        vstd::math::abs(self.u - other.u)
+    }
+
+    fn distance(&self, other: &Self) -> u64 {
+        if self.u > other.u {
+            self.u - other.u
+        } else {
+            other.u - self.u
+        }
+    }
+
+    proof fn valid_distance_metric() 
+    {
+    }
+}
+// ANCHOR_END: spec_trait_impl
+
+// ANCHOR: view_impl
+struct Stack {
+    data: Vec<u64>,
+}
+
+impl View for Stack {
+    type V = Seq<u64>;
+
+    closed spec fn view(&self) -> Seq<u64> {
+        self.data@
+    }
+}
+
+impl Stack {
+    fn push(&mut self, val: u64)
+        ensures final(self)@ == old(self)@.push(val),
+    {
+        self.data.push(val);
+    }
+
+    fn is_empty(&self) -> (result: bool)
+        ensures result <==> self@.len() == 0,
+    {
+        self.data.len() == 0
+    }
+}
+// ANCHOR_END: view_impl
+
+// ANCHOR: default_ensures
+trait Reducer {
+    // Every implementation must satisfy: output <= input.
+    // The default implementation additionally satisfies: output == input / 2.
+    fn halve(&self, input: u64) -> (output: u64)
+        ensures output <= input,
+        default_ensures output == input / 2,
+    {
+        input / 2
+    }
+}
+// ANCHOR_END: default_ensures
+
+// ANCHOR: default_ensures_impls
+struct DefaultReducer;
+
+impl Reducer for DefaultReducer {
+    // No override: inherits the default implementation and its default_ensures.
+}
+
+struct ThirdReducer;
+
+impl Reducer for ThirdReducer {
+    // Overrides with a different strategy.  Only the trait `ensures` (output <= input)
+    // applies to callers who don't statically know the type.
+    fn halve(&self, input: u64) -> (output: u64)
+        ensures output == input / 3,
+    {
+        input / 3
+    }
+}
+// ANCHOR_END: default_ensures_impls
+
+// ANCHOR: default_ensures_callers
+fn call_generic<H: Reducer>(h: &H, x: u64) {
+    let r = h.halve(x);
+    assert(r <= x);        // From trait ensures — always available
+    // assert(r == x / 2); // Would FAIL: not known for arbitrary H
+}
+
+fn call_default(h: &DefaultReducer, x: u64) {
+    let r = h.halve(x);
+    assert(r <= x);     // From trait ensures
+    assert(r == x / 2); // From default_ensures (DefaultReducer uses the default impl)
+}
+
+fn call_override(h: &ThirdReducer, x: u64) {
+    let r = h.halve(x);
+    assert(r <= x);        // From trait ensures
+    assert(r == x / 3);    // From ThirdReducer's own ensures
+    // assert(r == x / 2); // Would FAIL: ThirdReducer overrides, no default_ensures
+}
+// ANCHOR_END: default_ensures_callers
+
+} // verus!

source/docs/guide/src/SUMMARY.md

@@ -80,7 +80,7 @@
 - [Mutation, references, and borrowing](mutation-references-borrowing.md)
     - [Mutable references](mutable-references.md)
     - [Assertions about mutable references](assert-mut-ref.md)
-- [Traits]()
+- [Traits](traits.md)
 - [Iterator Specifications](./iterator-specs.md)
 - [Higher-order executable functions](./higher-order-fns.md)
     - [Passing functions as values](./exec_funs_as_values.md)

source/docs/guide/src/traits.md

@@ -0,0 +1,174 @@
+# Traits
+
+Verus supports writing specifications for trait functions, including `requires` and
+`ensures` clauses. Specifications on a trait function serve as a *contract* that all
+implementations must satisfy, and that callers can rely on when they call the function
+through a trait bound.
+
+For traits defined in external crates (e.g., from the Rust standard library), see
+[External trait specifications](./external_trait_specifications.md).
+
+## Trait function specifications
+
+Trait functions can have `requires` and `ensures` clauses just like ordinary functions:
+
+```rust
+{{#include ../../../../examples/guide/traits.rs:basic_trait}}
+```
+
+Any type implementing `Compressor` must provide a `compress` function whose body
+satisfies `output <= input`.
+
+## Extending specifications in implementations
+
+An implementation automatically inherits all `requires` and `ensures` clauses from the
+trait declaration.  Additionally:
+
+ * An `impl` **can** add stronger `ensures` clauses.
+ * An `impl` **cannot** add new `requires` clauses — that would be unsound, because a
+   caller using the trait bound `C: Compressor` has no obligation to satisfy
+   requirements that the trait doesn't mention.
+
+```rust
+{{#include ../../../../examples/guide/traits.rs:impl_extends}}
+```
+
+`HalfCompressor::compress` inherits `ensures output <= input` from the trait. 
+Verus verifies that the function's body satisfies both the inherited postcondition
+and the additional postcondition added by the implementation (`ensures output == input / 2`).
+
+A trait function can also include both `requires` and `ensures`:
+
+```rust
+{{#include ../../../../examples/guide/traits.rs:requires_ensures}}
+```
+
+```rust
+{{#include ../../../../examples/guide/traits.rs:requires_ensures_impl}}
+```
+
+## Generic vs. concrete dispatch
+
+When Verus can statically determine the concrete type of a trait function call, it uses
+the possibly-stronger specification from the `impl`.  When the call is through a generic
+type parameter, Verus only knows the trait-level specification.
+
+```rust
+{{#include ../../../../examples/guide/traits.rs:dispatch}}
+```
+
+## Spec and proof functions
+
+A trait may also contain `spec` and `proof` function declarations. 
+For example, the trait below requires implementations to provide 
+a distance metric (`dist`) as a specification function and then to prove that
+their `distance` function actually computes that metric.
+Moreover, the implementation must also prove (in its body for `valid_distance_metric`)
+that `dist` is a reasonable metric.
+
+```rust
+{{#include ../../../../examples/guide/traits.rs:spec_trait}}
+```
+
+Here's an example of an implementation of our `Distance` trait:
+```rust
+{{#include ../../../../examples/guide/traits.rs:spec_trait_impl}}
+```
+In this case, Verus can automatically prove all of the postconditions
+for `valid_distance_metric`, but a more complex distance metric might
+need additional proof annotations.
+
+Note that it's not necessary to repeat the requires/ensures that
+the implementation inherits from the trait definition.
+
+
+## The `View` trait
+
+The most commonly used trait in `vstd` is `View`.  It allows users to give
+executable types a mathematical abstraction (`type V`) accessed via the `view`
+function.  Since this is such a commonly invoked function, Verus provides the
+[`@` operator](reference-at-sign.md) as a shortcut, so that you can write `x@`
+instead of `x.view()`.
+
+```rust
+pub trait View {
+    type V;
+    spec fn view(&self) -> Self::V;
+}
+```
+
+`vstd` provides `View` implementations for common types:
+- `Vec<T>` → `Seq<T>`
+- `HashMap<K, V>` → `Map<K, V>`
+- `HashSet<K>` → `Set<K>`
+- Primitive types (`u64`, `bool`, etc.) → themselves
+
+To implement `View` for a custom type, choose an appropriate abstraction and
+then define `type V` and `spec fn view`:
+
+```rust
+{{#include ../../../../examples/guide/traits.rs:view_impl}}
+```
+
+Because `Stack`'s `data` is a private field, `view` is `closed` — callers cannot see its
+definition, but they can still reason about the effect each function has on that view,
+as illustrated by the postconditions on `push` and `is_empty`.  If you want
+callers to unfold `@` to its definition (e.g., for a `pub` type with a `pub`
+field), use `open spec fn view` instead.
+
+`vstd` also provides `DeepView`, which recursively applies the view abstraction
+to nested elements.  Most code only needs `View`.
+
+## `default_ensures`: specifications for default function implementations
+
+In Rust, a trait function can provide a *default implementation* — a body that
+implementations inherit if they do not override the function.  This creates a subtle
+specification problem: the trait-level `ensures` clause must be weak enough to allow
+any valid override, but the default body may satisfy a *stronger* postcondition.
+
+`default_ensures` solves this by separating these two concerns:
+
+```rust
+{{#include ../../../../examples/guide/traits.rs:default_ensures}}
+```
+
+Here the **trait-level `ensures`** (`output <= input`) is what any implementation must
+satisfy.  The **`default_ensures`** (`output == input / 2`) is an additional guarantee
+that holds *only* when a type uses the default implementation without overriding it.
+
+The rules:
+
+ * `default_ensures` is only allowed on a trait function that has a default body in the
+   trait declaration.
+ * `default_ensures` is checked against the default body just like a normal `ensures`.
+ * Callers that statically know the type inherits the default learn both `ensures` and
+   `default_ensures`; callers using a generic bound `T: Trait` learn only the `ensures`.
+
+```rust
+{{#include ../../../../examples/guide/traits.rs:default_ensures_impls}}
+```
+
+```rust
+{{#include ../../../../examples/guide/traits.rs:default_ensures_callers}}
+```
+
+When writing your own trait, consider using `default_ensures` on functions
+where a sensible default makes a stronger promise that custom implementations
+are not required to match.
+
+## Common `vstd` trait specifications
+
+`vstd` provides specifications for many standard library traits. A few worth knowing:
+
+ * **`PartialEq` / `Eq`** — `vstd` wraps these with an `obeys_eq_spec()` guard so that
+   only types that opt in are assumed to satisfy the functional equality contract.
+   See [External trait specifications](./external_trait_specifications.md) for the
+   `obeys_*` pattern.
+ * **`Iterator`** — `vstd` provides `IteratorSpecImpl` (not `Iterator` directly) for
+   writing specs on custom iterators.  See [Iterator Specifications](./iterator-specs.md).
+ * **`PartialOrd` / `Ord`** — similar to `PartialEq`, with `obeys_ord_spec()` guards.
+
+## External trait specifications
+
+For adding specifications to traits from external crates (including `std`), see
+[External trait specifications](./external_trait_specifications.md).