Next-generation of Tracked/Ghost code

[tjhance]

Over time, a number of challenges with the current Tracked/Ghost system have become apparent.

• Embedding Tracked/Ghost is confusing
• The need to put Tracked/Ghost in signatures and structs makes it difficult to verify 'existing' code
• Specs about Tracked code are ugly

I believe it is time to start sketching out the 'next generation', with an even greater separation of spec/proof & exec code.

Challenges with the current system

Embedding Tracked/Ghost in exec code is confusing

New users are always confused about how to use Tracked/Ghost and when they need to do it versus using tracked/ghost. This is understandable as the rules are pretty confusing, even if they follow logically from some implementation-constrained premises. The rules are documented here, and I frequently point users to this page, but I always feel a little embarrassed when I do so.

The need to put Tracked/Ghost in signatures and structs makes it difficult to verify 'existing' code

There are a number of problems here. For one, it makes Verus code look less familiar, e.g., you have to call vstd::raw_ptr::ptr_mut_write (which takes an extra tracked argument) instead of just writing *x = 5 which again makes it hard to explain what's going on. When you look at a verified function with a lot of ghost code, it can be hard to visually separate out what's what.

This is also a huge obstacle for verifying 'existing' code. Signatures and structs have to be modified internally, and if you want to apply a specification to an existing external function that requires extra ghost state, you have to create a wrapper function. Besides being inconvenient, @jonhnet has pointed out that implementing the wrapper function is confusing because the ghost operation is axiomatic, but you still have to construct the ghost state in the external_body function, which is a meaningless operation but is needed to satisfy the type-checker.

You also have to add stuff to structs, e.g., a doubly-linked list looks like:

    pub struct DoublyLinkedList<V> {
        head: Option<PPtr<Node<V>>>,
        tail: Option<PPtr<Node<V>>>,

        ptrs: Ghost<Seq<PPtr<Node<V>>>>,
        points_to_map: Tracked<Map<nat, PointsTo<Node<V>>>>,
    }   

Specs about Tracked code are ugly

Here's vstd::raw_ptr::ptr_mut_write:

pub exec fn ptr_mut_write<T>(
    ptr: *mut T,
    Tracked(perm): Tracked<&mut PointsTo<T>>,
    v: T,
)
    requires
        old(perm).ptr() == ptr,
        old(perm).is_uninit(),
    ensures
        perm.ptr() == ptr,
        perm.opt_value() == MemContents::Init(v),

Ugh! First you have to supply an extra perm argument, and then you have to write additional spec code about it. By contrast, in separation logic, the spec would look like:

∀ ptr, value, value’. { ptr ↦ value } *ptr = value’ { ptr ↦ value’ }

This looks nice and concise in part because it's written in terms of these universally quantified variables. This usually works out pretty well in something like Coq/Iris where the variables are usually inferred by coq's unification engine. In Verus, this kind of style is a lot harder to pull off. You can sort of systematically approximate it by adding extra Ghost params, but this sucks because (i) they look like Tracked variables even though their functional role is completely different and (ii) they then have to be supplied as arguments at the call-sites, i.e., it just exacerbates the previous 2 problems.

New approach sketch

Function signatures

First, tracked/ghost state should look entirely separate. I have no idea what the keywords / notation should be. But I imagine something isomorphic to:

pub exec fn ptr_mut_write<T>(
    ptr: *mut T,
    v: T,
)
    with (points_to: &mut PointsTo<T>)
    requires ... ensures ...

At the source level, this with clause now entirely looks like part of the spec. It should be possible to attach extra_tracked signatures to external_fn_specification specifications as well. To call this, the tracked arguments are visually separate:

ptr_mut_write(ptr, v)     with (&mut points_to);

With special cases for primitive Rust syntax:

*ptr = v     with (&mut points_to);

We can also separate out return values:

pub exec fn alloc() -> (ptr: *mut T)
    output (points_to: PointsTo<T>)
    requires ... ensures ...

And some kind of notation to deal with those at the call-site.

Tracked vs Ghost

We can have 2 different clauses types, one for ghost and one for Tracked params. Again, names TBD, but what I have in mind is that this:

fn foo()
   forall (x: X, y: Y)
   with (z: Z)
   requires ... ensures ...

Inference

Separating these params from the signature opens the door to do more inference, since these parameters won't be required by the surface-level type checker. In some circumstances, Verus may be able to fill them in. Admittedly, inferring tracked objects may be a Very Difficult (but rewarding) Problem. Inferring Ghost params should be a bit easier:

pub exec fn ptr_mut_write<T>(
    ptr: *mut T,
    new_val: T,
)
    forall (old_val: T)
    with (points_to: &mut PointsTo<T>)
    requires old(points_to)@ == PointsTo(ptr, Init(old_val)),
    ensures points_to@ == PointsTo(ptr, Init(new_val)),

Inspection of the requires clause shows that we can always infer old_val from points_to, so the caller wouldn't need to supply it.

Structs

Do something similar with structs. The doubly-linked list would look like:

    pub struct DoublyLinkedList<V> {
        head: Option<PPtr<Node<V>>>,
        tail: Option<PPtr<Node<V>>>,
    } with {
        ghost ptrs: Seq<PPtr<Node<V>>>,
        tracked points_to_map: Map<nat, PointsTo<Node<V>>>,
    }

This is equivalent to:

    pub struct DoublyLinkedList<V> {
        head: Option<PPtr<Node<V>>>,
        tail: Option<PPtr<Node<V>>>,
        ghost_state: Tracked<_GhostState<V>>,
    }
    pub tracked struct _GhostState<V> {
        ghost ptrs: Seq<PPtr<Node<V>>>,
        tracked points_to_map: Map<nat, PointsTo<Node<V>>>,
    }

And using the struct looks something like:

fn example() {
    let dlist = DoublyLinkedList { head: None, tail: None }
           with { ptrs: ..., points_to_map: ... };

    // Accessing a field needs some special notation
    dlist$.points_to_map
}

[ziqiaozhou]

But I am wondering whether it would be possible to make it closer to Rust style. For example, user can add proc-macro attributes on the functions that needs tracked variables.

#[with_tracked(points_to: &mut PointsTo<T>, ...)]
fn  ptr_mut_write(...)
{}

and pass the tracked variable similarly

#[with_tracked(&mut points_to, ...)]
ptr_mut_write(ptr, v);

and

[jaybosamiya-ms]

I think it'd be helpful to have a nicer-syntax version when you are inside the verus! macro, as well as support for attribute-based thing for when you might not be able to use the full-fledged macro in some codebase.

At a high level, I like the top-level idea introduced by @tjhance of not having to modify the core executable signature to support ghost and tracked variables being passed in and out, but yes, to @ziqiaozhou's point, we should definitely think about how this might work with both use cases.

[jaybosamiya-ms]

Overall, I really like the idea proposed at the top-level.

Regarding syntax, just thinking ahead for what might work well for parsers and such (ignore actual keywords, just focusing on structure), we probably want to think about binding strength, and attempting to keep things more prefix-focused, otherwise, it becomes hard to identify what this intends to mean:

*ptr = foo(a, b) with(&mut x);

If we instead make things prefixed, then there is an obvious difference between these two, and it is immediately clear which one the with applies to:

with(&mut x) *ptr = foo(a, b);
// AND
*ptr = with(&mut x) foo(a, b);

Essentially, by placing it in the prefix, it becomes tightly bound to the immediate next call or syntactic structure, rather than requiring large amount of look-ahead.

Once we move it to the prefix position, it almost looks like it is almost-trivial syntax sugar over attributes, which should hopefully keep implementation simple too.

Note: I also suggest playing return values within the with(...) as well, by prefixing them with out (e.g., with(&mut x, out y) baz(a, b);) to keep things easy to parse.

[parno]

I agree -- this seems like it could be a very nice improvement! I think dealing with return values seems like one of the trickier syntactic aspects. @jaybosamiya-ms: Using out as a signifier in the with clause it interesting. How would we distinguish between assigning the return value to an existing variable name vs. introducing a new variable name? It seems like both cases are relatively common. Would the latter end up as with (&mut x, let out y)?

[tjhance]

perhaps we should put inputs before teh command and outputs after (so it looks like a hoare triple)

with ( in <- xyz )
stuff();
out ( out1 -> x, out2 -> let y )

[jaylorch]

Breaking the assignment of return values into two lines sounds like a reasonable price to pay for the cool usability improvement @tjhance describes. Even for afficionados of long variable names like myself!

[parno]

I worry that putting out(...) after the semicolon may be confusing. Semicolon has a pretty strong connotation of "we just finished something and now we're moving on to something new". If we put out(...) before the semicolon, however, we run into @jaybosamiya-ms's parsing concerns.

Hence, I'm still tempted by @jaybosamiya-ms's suggestion of with(w, x, out y, let out z).

[tjhance]

I worry that putting out(...) after the semicolon may be confusing.

I have the opposite feeling, having thought about it a bit. In fact, I would now actually like to avoid tying these annotations directly to the nodes syntactically (as was my first instinct). This is a more ambitious mental shift, but I think this gives more flexibility in the long run.

There's a simple purity in writing a line like stuff();, or *a = 5;, each a complete statement, semi-colon and all, with proof annotations on the surrounding lines, whereas stuff() with (in blah, out foobar); remains in the Schrödinger state of having a line that is both proof and exec at the same time.

If the annotations are separate statements, this leaves us much more flexibility to write code "the way that we want"¹. For example, suppose we have the following simple exec statement:

let a = foo(stuff());

Now suppose we realize stuff() needs to return a new Tracked out-parameter. Oh no, now we have disrupt this entire foo line.

But what if we could just write this:

let a = foo(stuff());
MAGIC_PROOF_KEYWORD { out bar -> asdf }

In this case, Verus would work backwards from the MAGIC_PROOF_KEYWORD, see that the stuff() call has an out-param called bar and wire everything up for us.² With enough smarts, I think we can dramatically reduce proof annotations and have very normal-looking Rust code.

Footnotes

1. making all the implementations smaller and ruining all our proof-to-code metrics ↩

2. This is obviously more challenging to implement, and it has to be done by Verus proper rather than the macro. ↩

[parno]

Oh no, now we have disrupt this entire foo line.

This doesn't immediately seem like a disaster to me, although I can see how it might be a bit awkward to write

let a = foo(stuff() with (w, x, out y))

see that the stuff() call has an out-param called bar

To me, it seems a bit tedious for the developer to have to look up the names of the out parameters and add them at the call site as well.

Perhaps a useful exercise would be to a pick an existing file that already deals with a reasonable number of ghost and track arguments and out parameters, and then try rewriting it in both styles. That might clarify which version seems less cluttered and/or more readable.