Language Design, Macros

Code samples with Macros

Prusti-isms

use prusti_contracts::*;

#[pure]
fn divides(v: u64, u: u64) -> bool {
    exists!(|k: u64| k * u == v)
}

#[ensures(exists(|k: u64| k * result == a))]
#[ensures(exists(|k: u64| k * result == b))]
#[ensures(forall(|d: u64| exists(|ka: u64, kb: u64| ka * d == a && kb * d == b) ==> d <= result))]
fn gcd(a: u64, b: u64) -> u64 {
    unimplemented!() 
}

fn main() {
    let mut a = 0; let mut i = 3;
    while i > 0 {
        body_invariant!(i > 0 && a == 3 - i);
        a += 1; i -= 1;
    }
    assert!(i == 0);
}

Ideas by Andrea

spec!(
    fn divides(v: nat, u: nat) -> bool {
        exists(|k: nat| k * u == v)
    }
)
#[spec(
    ensures(exists(|k: nat| k * return == a)),
    ensures(exists(|k: nat| k * return == b)),
    ensures(forall(|d: nat| (divides(a, d) && divides(b, d)) ==> d <= return)),
)]
fn gcd(a: u64, b: u64) -> u64 {
    unimplemented!()
}
fn main() {
    let mut a = 0; let mut i = 3;
    #[spec(
        invariant(i > 0 && a == 3 - i),
        decreases(3 - i),
    )]
    while i > 0 {
        a += 1; i -= 1;
    }
    assert!(i == 0);
}

Ideas by @jaybosamiya

This version stays within Rust's syntax by placing things into macros (in particular the v! macro: an example definition of it is given below; in practice, one would want to use a proc-macro rather than a macro_rules-based macro though, for extensibility and greater control over the syntax). The version below can be compiled via rustc and all the annotations and such will immediately be removed (so essentially we get extraction "for free").

Using `macro_rules! v {...}` (Click to expand)

macro_rules! v {
    (state) => { () };
    (assert $($a:tt)*) => {};
    (assume $($a:tt)*) => {};
    (invariant ($($i:tt)*)
     decreases ($($d:tt)*)) => {};
    ($ty:ty
     $(| requires ($($req:tt)*))?
     | ensures (|$res:tt| {$($ens:tt)*})
     $(| decreases ($($dec:tt)*))?
    ) => {
        $ty
    };
}

fn foo(x: u64) -> v!(
    u64
    | requires (x < u64::MAX)
    | ensures (|r| {r == x + 1 && r <= u64::MAX})
) {
    x + 1
}

fn bar(
    l: &mut Vec<u64>,
    n: usize,
    v: u64,
) -> v!(
    ()
    | ensures (|()| {
        forall i. if 0 <= i && i < l.len() {
            if i <= n {
                l[i] == v
            } else {
                l[i] == old(l)[i]
            }
        }
    })
    | decreases (n)
) {
    let _st1 = v!(state);
    if n < l.len() {
        l[n] = v;
    }
    v!(assert {
        forall i. if n <= i && i < l.len() {
            if i <= n {
                l[i] == v // Current version of `l`
            } else {
                l@_st1[i] == old(l)[i] // Can explicitly refer to a specific `l`
            }
        }
    });
    let _st2 = v!(state);
    if n > 0 {
        bar(l, n - 1, v);
    }
    v!(assume false); // Eg: I am too lazy to prove this :P
}

fn baz() {
    let mut a = 0; 
    let mut i = 3;

    while i > 0  {
        v!(invariant (i > 0 && a == 3 - i) decreases (3 - i));
        a += 1;
        i -= 1;
    }
    v!(assert i == 0); // verification/static assert
    assert!(i == 0); // runtime assert (already exists in Rust)

    println!("{}", a);
}

The above syntax has some warts due to implementing it via macro_rules rather than a proc-macro which would allow arbitrary token streams within the macro. Nonetheless, it is a reasonable approximation of what might be doable with macros.

Sidenote: The loop invariant within the body of the while loop is actually a feature, not a bug. For v1, we might want to restrict it to only be at the start of the body, but as a v2 idea, we might want to allow it to float anywhere in the body (and use weakest-preconditions to figure out the actual invariant at the head of the loop). Most people would want to use loop invariants only at the head, but in certain (admittedly rare) situations, a loop invariant in the middle of the loop is actually a more "natural" place to put it. By leaving it inside the loop, we allow for this sort of "floating" invariant in the future.

Another sidenote: Looks like these macros already confuse GitHub's syntax highlighting 🙃