Hello everyone!

This is going to be a quick one.

What even is a specification?

Yesterday I was messing around a bit with formal verification, and trying to figure out what exactly is the difference between “how” you do something and “what” is the thing you want to do (in software). This is an interesting question because a “specification” is usually described as something that says “what” you want to do a piece of software to do, as opposed to “how”.

However, this never made sense to me. The difference in “how” and “what” is simply the level of detail you use to describe the thing, and modern software all depend on a compiler interpreting your intent and writing something else that actually implements that - in other words, no programmer actually knows the “how”, just the “what”.

This led to a long conversation in the Doom Emacs Discord channel that ended up pointing me to a few interesting resources:

• Conal Elliott
• Bird-Maeertens formalism

But it also seemed to confirm my suspicions: implementation is just the end of the spectrum of specification¹ and a “fully” specified specification can only have a single implementation, by definition.

This was all very interesting to me but the reason I was looking into this stuff was trying to figure out when exactly does a set of tests actually become a specification, because an intuition that I have is that specifications are usually just a “compressed” way of describing tests that can then be “analysed” as opposed to just executed.

Hence, I wanted to see how exactly this “specifications as tests” thing would look like in a real language².

Now with gusto, I mean, Rust

Enter Prusti, a formal specification and verification tool for Rust 🦀.

Here’s a simple example of how it works:

use prusti_contracts::*;

// Cheating is life.
// Prusti doesn't know about signum()
#[trusted]
#[ensures(n < 0 && result == -1 ||
          n > 0 && result == 1 ||
          n == 0 && result == 0)]
fn sign(n: i64) -> i32 {
    n.signum() as i32
}

// Specification
#[ensures(a > b && result == a ||
          b > a && result == b ||
          result == a && result == b)]
// A weird implementation
fn max(a: i32, b: i32) -> i32 {
    let s = (-sign(a as i64 - b as i64) + 1) / 2;

    (a - a * s) + b * s
}

// Actually executing programs is overrated
fn main() {}

In English:

1. Cheat a bit by letting Prusti know about how the sign() function works.
2. Specify the behaviour (i.e.: emergent properties) we want out of the max() function.
3. Implement it in the most convoluted way possible for the sake of the example.

And now we can prove this is all good and beautiful:

❯ prusti-rustc --edition=2021 prusti.rs
  __          __        __  ___             
 |__)  _\/_  |__) |  | /__`  |   ____\/_  | 
 |      /\   |  \ \__/ .__/  |       /\   | 

Prusti version: 0.2.2, commit 4a9a39c 2023-05-23 17:14:43 UTC, built on 2023-05-27 12:47:41 UTC
warning: function `sign` is never used
  --> prusti.rs:10:4
   |
10 | fn sign(n: i64) -> i32 {
   |    ^^^^
   |
   = note: `#[warn(dead_code)]` on by default

warning: function `max` is never used
  --> prusti.rs:19:4
   |
19 | fn max(a: i32, b: i32) -> i32 {
   |    ^^^

Verification of 3 items...
Successful verification of 3 items
warning: 2 warnings emitted

❯ 

Wow 🤯 who would have thought max() really works! Absolutely mind blowing!

Seeya 🦀 *leaves walking sideways*