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.

[ziqiaozhou]

BTW, attribute macros follow the new style to use tracked/ghost code, but the way to pass the ghost variable could be benefited by a real functin-based ghost argument passing.

#1492
#1603

#[verus_spec(ret =>
    with
        Tracked(y): Tracked<&mut u32>,
        Ghost(w): Ghost<u32>,
        ->  z: Ghost<u32>
    requires
        x < 100,
        *old(y) < 100,
    ensures
        *y == x,
        ret == x,
        z@ == x,
)]
fn test_mut_tracked(x: u32) -> u32 {
    proof!{
        *y = x;
    }
    proof_with!{|= Ghost(x)}
    x
}

#[verus_spec]
fn test_cal_mut_tracked(x: u32) {
    proof_decl!{
        let ghost mut z = 0u32;
        let tracked mut y = 0u32;
    }
    proof_with!{Tracked(&mut y), Ghost(0) => Ghost(z)}
    let x = test_mut_tracked(1);
    if x == 0 {
        proof! {
            assert(z == 1);
        }
        return;
    }

    proof!{
        assert(y == 1);
    }
}

[Chris-Hawblitzel]

We've been using call_requires<Args, F> and call_ensures<Args, F> for exec Fn values. Should we have something like call_requires_with<Args, F, In> and call_ensures_with<Args, F, In, Out> for Fn values that need extra with inputs and outputs?

[ziqiaozhou]

In #2436 I do need call_requires_with and call_ensures_with that allow extra inputs and outputs. That PR does not cover that yet. Instead, just panic when trying to call call_requires/ensures for a function takes extra input/outputs.

[mkovaxx]

Recording and synthesizing a few ideas from the Verus Retreat:

• (@bsdinis) Automate plumbing of tracked/ghost values.
• (@dschoepe) Separate the concerns of definition and call-site syntax.
• Keep call-site syntax simple and consistent. Add syntax sugar on top.

Mental model to reason about the feature when it comes to call sites. This is independent of the syntax used to define a function involving tracked/ghost values. While it makes sense to separate tracked/ghost values in a function's signature, the benefit of doing so at a call site seems small compared to the added complexity.

Notionally, a function f with tracked/ghost values in its signature always comes in two flavors: an "erased" f with all tracked/ghost values absent from the signature, and a tracked_f with tracked/ghost values present in the signature.

Example function and its notional signatures:

// defined in the current syntax
fn f(x: f32, y: f32) -> f32
    with (tracked tr: bool, ghost gh: u8),
    output (ghost i32, f32),
{ ... }

// tracked `f` signature
fn tracked_f(x: f32, y: f32, tr: Tracked<bool>, gh: Ghost<u8>) -> (f32, Ghost<i32>, Tracked<f32>);

// erased `f` signature
fn f(x: f32, y: f32) -> f32;

Primary goal: explicitly mark each call site syntactically.

For example, the tracked keyword could be reused to mark call sites (see alternatives below):

let x: f32 = ...;
let y: f32 = ...;
let tracked tr = ...;
let ghost gh = ...;

// call `f` as erased (in non-verified code)
let z = f(x, y);

// call `f` as tracked (in verified code)
let (z, ghost i, tracked w) = tracked f(x, y, tr, gh);

Secondary goal: provide syntactic sugar to automate plumbing.

For example, when a tracked function has only one input, support automatically "unpacking" the tracked/ghost arguments from a tuple, e.g. the result of another call.

Given another function g with tracked and erased signatures:

// tracked `g` with tracked/ghost values present in the signature
fn tracked_g(z: f32, i: Ghost<i32>, w: Tracked<f32>) -> bool;

// erased `g` with tracked/ghost values absent from the signature
fn g(z: f32) -> bool;

That syntactic sugar would allow the following shorthand form:

// sugary syntax
let flag = tracked g(tracked f(x, y, tr, gh));

// desugars into
let flag = {
    let (z, ghost i, tracked w) = tracked f(x, y, tr, gh);
    tracked g(z, i, w)
};

Syntax Bikeshed Alternatives

Instead of prefixing the call, the tracked keyword could separate (and group) the tracked/ghost arguments:

// separator
let (z, tracked i, w) = f(x, y, tracked tr, gh);
let flag = g(f(x, y, tracked tr, gh));

// pseudo-function / tuple struct
let (z, tracked(i, w)) = f(x, y, tracked(tr, gh));
let flag = g(f(x, y, tracked(tr, gh)));

// pseudo-struct
let (z, tracked { i, w }) = f(x, y, tracked { tr, gh });
let flag = g(f(x, y, tracked { tr, gh }));

Could also use the with keyword instead:

// separator
let (z, with i, w) = f(x, y, with tr, gh);
let flag = g(f(x, y, with tr, gh));

// pseudo-function / tuple struct
let (z, with(i, w)) = f(x, y, with(tr, gh));
let flag = g(f(x, y, with(tr, gh)));

// pseudo-struct
let (z, with { i, w }) = f(x, y, with { tr, gh });
let flag = g(f(x, y, with { tr, gh }));