verus
forked from verus-lang/verus
Star 0
Fork 0
Watch
verus source docs guide src iterator-specs-infinite.md
5.0 kB · 110 lines
Markdown
at master

Implementing Iterator Specifications for Infinite Iterators #

Somewhat surprisingly, we can also follow the same steps needed to verify an iterator implementation for a custom type that implements an infinite iterator!

Let's start with an infinite iterator built on a counter that increments each time we call next(), wrapping when we would otherwise overflow.

1. The iterator struct #

IterCtr holds the 64-bit counter value (count), and a prophetic length field that defines how long the sequence of return values will be. At this point, we don't know what the length is; we just know it has some value.

{{#include ../../../../examples/guide/iterators.rs:ctr_iter_def}}

2. The next method #

This is an ordinary Rust Iterator implementation. However, we do need to include a proof that next() meets its obligations, especially the obligation that the value returned by next() matches the first element in the prophesized remaining sequence. Here, the key idea is to swap the existing prophecy variable (in self.len) with a newly created prophecy variable. We then resolve the old prophecy variable in such a way that its final value is one more than the prophecy variable we just created. This is enough to show that the prophetic sequence's length decreased by one, just as the spec for next() demands.

{{#include ../../../../examples/guide/iterators.rs:ctr_normal_iter}}

3. The spec implementation #

In vstd, Verus provides IteratorSpec, an extension of the Rust Iterator trait that defines a variety of specification functions, as well as the Verus specs for the next() function. To enable us to reason about our custom iterator, we need to implement the Verus-provided IteratorSpecImpl trait (not the IteratorSpec trait that defines the specs -- see "External trait specifications" for more details). The discussion of finite iterators describes the purpose of each of these functions. Here's how we define them for our custom iterator.

  • obeys_prophetic_iter_laws — We return true, since our implementation is verified to obey the specs prescribed by IteratorSpec.
  • remaining — Our prophetic sequence has some (unknown) length predicted by self.len. The contents are simply the current value of the counter, incremented by 1 at each step and wrapping after u64::MAX.
  • produces — We will always return a value when next is call, so we set all of the indices to true.
  • decrease — This is an infinite iterator, so we don't have a valid decreases metric available, so we return None.
  • peek — It's simple to predict what this value will be, and it helps improve automation, so we return Some with the appropriate value.
{{#include ../../../../examples/guide/iterators.rs:ctr_iter_spec}}

4. The constructor #

Our constructor's postconditions are simpler than in the finite case, since we don't need to promise the iterator will terminate.

Example Usage #

Here's a small example that makes use of our new infinite iterator:

{{#include ../../../../examples/guide/iterators.rs:ctr_usage_example}}

Naturally we need to use the exec_allows_no_decreases_clause attribute, since this loop will never terminate.

Soundness #

It may initially seem troubling that we can specify the outputs of an infinite iterator with a finite sequence. One way to understand what's happening in this example is that at each program point, we're quantifying over "all sequences that don't contradict the prefix that has been observed so far". That set remains non-empty no matter how long the program executes.

Implementing DoubleEndedIterator #

We can extend this idea even further to support infinite iterators that nonetheless implement Rust's DoubleEndedIterator trait. Here's an example where next() always returns 42 and next_back() always returns 43. Instead of prophesizing one length, we prophesize the number of 42s and the number of 43s we'll return:

{{#include ../../../../examples/guide/iterators.rs:inf_dbl_def}}

We then use the two prophecies to give the natural definition of remaining:

{{#include ../../../../examples/guide/iterators.rs:inf_dbl_spec}}

As a result, the implementations of next() and next_back() are straightforward, following the earlier example above and using the same "trick" of swapping in a new prophecy variable whose value is one less than the old prophecy variable.

See the full file for more details.