Autoview

[utaal]

I think we should make autoview behave more like Rust's autoderef. With the current autoview, if the following is defined for Vec<T>

fn view(&self) -> Seq<T>

impl Vec<T> {
  #[verifier(autoview)]
  fn len(&self) -> u64 { ... }
}

and Seq<T> has

impl Seq<T> {
  fn len(&self) -> nat { ... }
}

Then, in a #[spec] context, when v: Vec<T>, then v.len() is automatically desugared to v.view().len().

---

I propose two changes. The first, I think, uncontroversial.

1. View trait

Define a new View trait that declares the fn view(&self) -> T function, instead of depending on the compiler finding a function named view in the impl.

trait View {
  type Viewed; // The type of the view

  fn view(&self) -> Viewed;
}

For the Vec<T> example, autoview(&self) should be replaced with:

impl View for Vec<T> {
  type Viewed = Seq<T>;

  #[spec] fn view(&self) -> Seq<T> { ... }
}

2. Autoview functions not tagged with #[autoview]

We should also consider to autoview functions that don't have an exec/proof counterpart, e.g.

enum Tree {
    Nil,
    Node { value: i64, left: Box<Tree>, right: Box<Tree> },
}

impl View for Tree {
  type Viewed = Seq<int>;

  #[spec] fn view(&self) -> Seq<int> {
    decreases(self);
    match *self {
        Tree::Nil => seq![],
        Tree::Node { value, left, right } => left.view().add(seq![value as int]).add(right.view()),
    }
  }
}

Now, len is defined on Seq<int>, but not on Tree, as it wouldn't make sense there.

When t: Tree, I think we should still automatically desugar t.len() to t.view().len() (or t.index(idx) to t.view().index(idx)) in a #[spec] context. This behaviour would match that of rust's autoderef.

API discoverability, potential for ambiguity

There may be a concern that it's harder to find the definition of autoviewed functions. However, the View trait impl for a type immediately points to the view type (Viewed), making it trivial to lookup (in the fullness of time, we could highlight it in the emitted rustdoc).

Additionally, because autoview is only applied in spec contexts, where calling proof or exec functions isn't possible, there's no risk of confusion for the user: they can expect every call to be to either a spec function on the concrete type, or a spec function on the view. In case a spec function with the same name is present both in the concrete type, and the view type (which we should discourage), we would never autoview that function and require the user to write t.view().func().

Convenience

In implementing the binary tree functions for chapter 1, exercise 22 of the summer school, https://github.com/secure-foundations/verus/blob/main/source/rust_verify/example/summer_school/chapter-1-22.rs#L77-L222 @jonhnet and I found that it was always natural to think of the tree as its view (a Seq) in spec contexts, and we would have liked to be able to leave off the call to .view() for .index(idx), .last(), and .len(). It never felt ambiguous whether we would be calling functions on the Tree or view Seq<int> because it was obvious which functions related to a sequence instead of a tree.

In this example, it would have been pretty burdensome to get this behavior with the current restrictions. We would have needed implementation stubs on Tree for index, len, and last (and any other function on Seq we may have wanted to call.

impl Tree {
  #[verifier(autoview)]
  fn len(&self) -> usize { unimplemented!() }

  #[verifier(autoview)]
  fn index(&self, i: usize) -> i64 { unimplemented!() }

  #[verifier(autoview)]
  fn last(&self) -> i64 { unimplemented!() }
}

Reuse

Removing the restriction that a function exists on the concrete type also facilitates reuse of the types used as views, like in the Tree -> Seq<int> example above. A user can pick an existing type for the Viewed view type without having to worry about the interactions with the functions in the concrete type.

Traits that support Rust features

With the current rules for autoview, I believe it's also awkward to support traits that support Rust features such as Index. I think it makes perfect sense, for t: Tree, to be able to write t[0] in a spec context to access the first element of its Seq representation; but that would currently require more boilerplate:

impl Index<u64 /* unclear what type would even go here */> for Tree {
  type Output = i64;

  #[verifier(autoview)]
  fn index(&self, idx: u64) -> &Self::Output { unimplemented!() }
}

With the proposed rules, this impl block is not needed.

[utaal]

We discussed this in the group meeting.

The consensus is to go ahead and only use the implementation of the View trait as a signal to attempt auto-view in spec contexts. To avoid ambiguity with a potential chain of Derefs, we are currently planning to only perform autoderef in non-spec contexts, and only attempt autoview in spec contexts.