Add documentation for trait extensions

examples/guide/external_trait_specs.rs

@@ -0,0 +1,88 @@
+#[allow(unused_imports)]
+use verus_builtin::*;
+#[allow(unused_imports)]
+use verus_builtin_macros::*;
+
+// ANCHOR: basic_trait
+#[verifier::external]
+trait Encoder {
+    fn encode_value(&self, x: u64) -> u64;
+}
+// ANCHOR_END: basic_trait
+
+verus! {
+
+// ANCHOR: basic_spec
+#[verifier::external_trait_specification]
+trait ExEncoder {
+    // This associated type names the trait being specified:
+    type ExternalTraitSpecificationFor: Encoder;
+
+    fn encode_value(&self, x: u64) -> (result: u64)
+        ensures
+            result >= x;
+}
+// ANCHOR_END: basic_spec
+
+// ANCHOR: basic_use
+fn use_encoder<E: Encoder>(f: &E, val: u64) -> (result: u64)
+    ensures
+        result >= val,
+{
+    f.encode_value(val)
+}
+// ANCHOR_END: basic_use
+
+} // verus!
+
+verus! {
+
+#[verifier::external]
+trait Summarizer {
+    fn summary(&self) -> (result: u64);
+}
+
+// ANCHOR: extension_spec
+#[verifier::external_trait_specification]
+#[verifier::external_trait_extension(SummarizerSpec via SummarizerSpecImpl)]
+trait ExSummarizer {
+    type ExternalTraitSpecificationFor: Summarizer;
+
+    // A spec helper function (not part of the original trait):
+    spec fn spec_summary(&self) -> u64;
+
+    fn summary(&self) -> (result: u64)
+        ensures
+            result == self.spec_summary();
+}
+// ANCHOR_END: extension_spec
+
+// ANCHOR: extension_impl
+struct MyCustomStruct { value: u64 }
+
+// Implement the concrete external Summarizer trait
+impl Summarizer for MyCustomStruct {
+    fn summary(&self) -> u64 {
+        // Prove that our overly complicated implementation satisfies the spec_summary
+        let v = self.value;
+        assert(v & 0xffff_ffff_ffff_ffff == v) by (bit_vector);
+        v & 0xffff_ffff_ffff_ffff
+    }
+}
+
+// Implement the additional spec functions
+impl SummarizerSpecImpl for MyCustomStruct {
+    spec fn spec_summary(&self) -> u64 {
+        self.value
+    }
+}
+
+fn test_hasher(h: &MyCustomStruct) {
+    let v = h.summary();
+    assert(v == h.value);
+}
+// ANCHOR_END: extension_impl
+
+} // verus!
+
+fn main() {}

source/docs/guide/src/SUMMARY.md

@@ -168,6 +168,7 @@
     - [recommends](./reference-recommends.md)
   - [Traits and signature inheritance](./reference-signature-inheritance.md)
   - [Specifications on FnOnce](./reference-signature-fnonce.md)
+- [External trait specifications](./external_trait_specifications.md)
 - [Loop specifications]()
   - [invariant]()
   - [invariant_except_break / ensures]()

source/docs/guide/src/calling-unverified-from-verified.md

@@ -105,38 +105,6 @@ This declaration makes Verus aware of the type `SomeStruct` and all its fields (
 
 ## Adding specifications for external traits
 
-Similar to the examples above, suppose there is an external trait `T`:
-```rust
-#[verifier::external]
-trait T {
-    fn f(&self, q: &Self, b: bool) -> usize;
-    type X;
-}
-```
-You can add a specification to `T` as follows:
-```rust
-#[verifier::external_trait_specification]
-trait ExT {
-    type ExternalTraitSpecificationFor: T;
-
-    fn f(&self, q: &Self, b: bool) -> (r: usize)
-        requires
-            b,
-        ensures 
-            r > 7,
-        ;
-    type X;
-}
-```
-Here, the specially named associated type `ExternalTraitSpecificationFor` specifies which trait is being specified.  With this specification in place, verified code can use the trait `T` and the members `f` and `X` of `T`, and any uses of `T::f` will be verified based on the specification provided by `ExT::f`.  For example:
-```rust
-        fn test<A: T>(a: &A) {
-            let i = a.f(a, true);
-            assert(i > 7);
-            let i = a.f(a, false); // Precondition fails
-        }
-```
-
-The external trait specification is not required to include all members of the trait.  Members that are not included are not accessible to verified code.
+You can also add specifications to external traits using the `#[verifier::external_trait_specification]` attribute. This lets you add `requires` and `ensures` clauses to trait methods, and optionally define spec helper functions with `#[verifier::external_trait_extension]`.
 
-**WARNING:** Be very cautious when adding specifications to trait functions in this manner!  All reachable and unreachable implementations of the trait are assumed to uphold the trait specifications. For example, if you verify a crate with `pub fn test<A: T>(...)`, we assume that whatever type instantiates `A` will uphold the specification for `T`, even if this type comes from an unverified crate that hasn't been written yet. In other words, this is a contract on both current and future unverified code that must be satisfied to correctly link unverified code with verified code.
+For details and examples, see [External trait specifications](./external_trait_specifications.md).

source/docs/guide/src/external_trait_specifications.md

@@ -0,0 +1,120 @@
+# External trait specifications
+
+When writing verified code that interacts with external Rust libraries, you may need
+to add specifications to traits defined in those libraries. Verus provides two attributes
+for this purpose:
+
+ * `#[verifier::external_trait_specification]` — adds requires/ensures to trait methods
+ * `#[verifier::external_trait_extension]` — additionally defines spec helper functions on the trait
+
+## Soundness warning
+
+**Be cautious when adding specifications to external traits.** All implementations
+of the trait — including those in unverified code, even code that hasn't been written yet — are
+assumed to uphold the specification. For example, if you verify a crate with
+`pub fn test<A: Formatter>(...)`, Verus assumes that whatever type instantiates `A` will
+satisfy the `Formatter` specification, even if that type comes from an unverified crate.
+This is a contract on both current and future unverified code.
+
+[See below](the_obeys_pattern_in_vstd) for a useful pattern (employed by `vstd`) for mitigating this soundness risk.
+
+## Basic external trait specification
+
+Suppose we have an external trait:
+
+```rust
+{{#include ../../../../examples/guide/external_trait_specs.rs:basic_trait}}
+```
+
+We can add specifications to it with `#[verifier::external_trait_specification]`:
+
+```rust
+{{#include ../../../../examples/guide/external_trait_specs.rs:basic_spec}}
+```
+
+Key points about this syntax:
+ * The specification trait (here `ExEncoder`) must contain a specially named associated type
+   `ExternalTraitSpecificationFor` whose bound names the external trait being specified.
+ * The trait name `ExEncoder` is arbitrary and is not used elsewhere.
+ * Method signatures must match the external trait, but you can add `requires` and `ensures` clauses,
+   and you can give a name to the return value (e.g., `(result: u64)`) for use in `ensures`.
+ * The specification trait is not required to include all members of the external trait.
+   Members that are not included are not accessible to verified code.
+
+With the specification in place, verified code can use the trait:
+
+```rust
+{{#include ../../../../examples/guide/external_trait_specs.rs:basic_use}}
+```
+
+## External trait extension (spec helper functions)
+
+Sometimes, a trait specification needs additional spec-mode functions that don't
+exist in the original trait. For example, you may want a spec function that describes the
+abstract behavior of a method. The `#[verifier::external_trait_extension]` attribute supports this.
+
+The attribute takes the form:
+```
+#[verifier::external_trait_extension(SpecTrait via SpecImplTrait)]
+```
+
+ * **SpecTrait** is the name of a spec-mode trait that becomes available in verification.
+   It is automatically implemented for any type implementing the external trait.
+ * **SpecImplTrait** is the name of a trait that concrete types implement to define the
+   spec helper functions.
+
+Here is an example, using a fictitious external trait named `Summarizer`:
+
+```rust
+{{#include ../../../../examples/guide/external_trait_specs.rs:extension_spec}}
+```
+
+Concrete types implement `SpecImplTrait` (here `SummarizerSpecImpl`) to define the spec helpers,
+and can then use the specifications in verified code:
+
+```rust
+{{#include ../../../../examples/guide/external_trait_specs.rs:extension_impl}}
+```
+
+## The `obeys_*` pattern in `vstd`
+
+`vstd` uses `external_trait_extension` extensively for standard library traits like `PartialEq`,
+`Ord`, `Add`, `From`, etc.  These specifications follow a common pattern using an `obeys_*`
+spec function that indicates whether a given type implementation actually follows the
+specification.
+
+For example, `vstd`'s specification for `PartialEq` looks roughly like this:
+
+```rust
+#[verifier::external_trait_specification]
+#[verifier::external_trait_extension(PartialEqSpec via PartialEqSpecImpl)]
+pub trait ExPartialEq<Rhs = Self> {
+    type ExternalTraitSpecificationFor: PartialEq<Rhs>;
+
+    spec fn obeys_eq_spec() -> bool;
+    spec fn eq_spec(&self, other: &Rhs) -> bool;
+
+    fn eq(&self, other: &Rhs) -> (r: bool)
+        ensures
+            Self::obeys_eq_spec() ==> r == self.eq_spec(other);
+}
+```
+
+The ensures clause says: **if** the type obeys the Verus spec for `Eq` (`obeys_eq_spec()` is true), **then**
+the result matches `eq_spec`. For integer types and `bool`, `vstd` defines `obeys_eq_spec()`
+to be true, and proves that these types satisfy the `eq_spec`.  For other types, Verus
+doesn't know whether `obeys_eq_spec()` is true or false, so it won't assume that the postcondition
+holds.  This pattern lets `vstd` provide useful specifications for well-behaved types without making
+unsound assumptions about all types.  If you want to use a trait like `Eq` for an external type,
+you can use an [`assume_specification`](./reference-assume-specification.md)
+to say that `obeys_eq_spec()` is true.
+
+## Rules and restrictions
+
+ * The `ExternalTraitSpecificationFor` associated type is required and must name the
+   external trait.
+ * The specification trait should not have a body for any method.
+ * Generic parameters and associated types must match the external trait exactly.
+ * When using `external_trait_extension`, the two names (`SpecTrait` and `SpecImplTrait`)
+   become real trait names that can be used in bounds and `impl` blocks.
+