linearity & the ergonomics of proof-mode maps

[tjhance]

Setting up the problem

Experience in LinearDafny using glinear map demonstrated a need for much more ergonomic ways to manipulate glinear map objects. ('proof' objects in Verus parlance)

Let's start with a few motivating examples (let P be a proof type object). All of these were the sorts of things to come up in our LinearDafny work, but they were very cumbersome to handle.

• Example 1: We have a map<int, P> with domain 0..n, but we want to 'shift' all the elements by 1, e.g., get a map with domain 1..n+1, but with the same elements in it.
• Example 2: We have 2 maps a: map<K, P> and b: map<K, P> with disjoint domains and want to take the union.
• Example 3: The opposite of example 2: We have a single map, but want to split it in two.
• Example 4: Given a map map<K, P> and a (proof-mode) function P -> Q, we want to apply that function to all values and obtain a map map<K, Q>.

In a "spec" world, we would accomplish such operations using simple map comprehensions.

// Example 1
let m : map<int, V>
let n = map_comp(|k| 1 <= k <= n+1 :: m.get(k - 1))

Doing this in the "proof" world, i.e., where m is a proof variable, suddenly raises questions. If the expression in the "value" position of the mapcomp is proof mode, how do we ensure m is used safely?

Example 3 poses additional challenges, where a single variable would apparently be consumed by multiple different statements:

// Example 3
let u : map<int, V>
assume A, B disjoint
let a = map_comp(|k| k \in A :: u.get(k))
let b = map_comp(|k| k \in B :: u.get(k))

The user wants to write code that looks like the above while having Verus check that it's safe.

Ideally, failure cases would have nice error messages:

let n = map_comp(|k| 1 <= k <= n+1 :: m.get(f(k)))
                                      ^^^^^^^^^^^ cannot show that f(k1) != f(k2) for distinct k1, k2

let a = map_comp(|k| k \in A :: u.get(k))
                                ^^^^^^^^
let b = map_comp(|k| k \in A :: u.get(k))
                                ^^^^^^^^ cannot show that these two calls to `get` will have distinct indices

Goals

• To be able to 'bend' the borrow-checker, so that a proof-type map m can be used more than once, with Verus checking by SMT that no index is consumed more than once.
• To accomplish this without the user having to update state by explicitly "removing" elements from the map as they are consumed.
• To have all this checking operate properly with map comprehensions
• To have all this checking operate properly with basic control flow
• Precise error messages on failure, regarding which indices intersected

In effect, it would be as if the linearity-checker applied to each element u.get(i) individually.

Proposed implementation

There are a lot of components to the "implementation" of the idea, including the user interaction (how do they activate the feature), how a function like m.get(i) would even be specified, how does VC gen work, and how do we get Rust's borrow checker to do the right thing.

(Since this is all proof (i.e., ghost) code, we don't have to worry about executable code for any of this.)

First, the user would write something like this, using a new Verus primitive called "scatter":

scatter(&mut m);
let a = m.get(0);
let b = m.get(1); // Verus creates proof obligation that 0 != 1

Naturally, m.get would need to be some trusted function with some special verifier attribute so that Verus knows that it's special.

m.get would also need to take m as a normal immutable borrow type, to make sure that the borrow checker doesn't complain. The scatter line ensures that m is actually available at that point, and then Verus would have to check that m is not used at any point afterwards (in non-spec code) except by calling m.get(...) and only in ways that Verus actually knows how to handle.

VCs are not too bad, provided we bail out if we encounter loops or anything complex. As we walk through, we collect 'sets' of indices that have been used (these could be explicit set objects, or sets represented implicitly by predicates), and require them to all be disjoint. Map comps also need to check that distinct "iterations" of the map comp don't overlap.