Specification language discussion

[avadacatavra]

At the Rust All Hands in Berlin, we discussed creating a specification language that would be a subset of Rust to use for specifying conditions/constraints/contracts in Rust programs.

We need

• Your thoughts on a Rust spec language
• Examples of specifications we might want to write

[vakaras]

I think we could start with something like:

• Use preconditions and postconditions as attributes on top level constructs. For example:

  #[ensures="result >= a && result >= b"]
  fn max(a: i32, b: i32) -> i32 {
      if (a < b) { b } else { a }
  }
  

• Use macros to specify loop invariants anywhere in the loop body:

  while random() {
      // do something
      invariant!(some_boolean_expression);
      // do something else
  }
  

  The main motivation for allowing this is that it does seem that a more restrictive version where we require the loop invariant to be at a specific point would not be easier to implement for verifiers that require loop invariants and work at MIR or lower levels (probably, currently it is only Viper?).

• Have two types of assertions: basic and tool specific.

  • A basic assertion would be a boolean Rust expression that uses only the constructs that are allowed in Java expressions. For example, I think that we should not allow loops in assertions. Also, we should not allow functions that have side effects in assertions (we still need to define what side-effect-free means).
  • We should find a way how tools could extend the specification language with tool specific constructs such as quantifiers.

[asajeffrey]

Is there any chance we could use quickcheck-style properties? Something like:

#[verify]
fn max_is_ok(x: i32, y: i32) {
    let z = max(x, y);
    assert!(x <= z);
    assert!(y <= z);
}

this would save putting arbitrary Rust expressions in attributes, and might interoperate better with test environments?

[vakaras]

@asajeffrey Viper does a procedure-modular and loop-modular verification, which means that you need to put specifications on all functions and loops. Therefore, I think that using the syntax from your example would be quite inconvenient. By the way, is there any reason why quickcheck could not use the syntax from my example?

[asajeffrey]

@vakaras I can understand why we need tool-specific ways for users to give hints to tools, e.g. pre/postconditions, loop invariants etc. I'm just wondering if there's some way we can specify the properties that are being verified in a way which is amenable to lots of different verification strategies.

The API for quickcheck is at https://github.com/BurntSushi/quickcheck, the annotations there are things like:

#[quickcheck]
fn max_is_ok(x: i32, y: i32) -> bool {
    let z = max(x, y);
    (x <= z) && (y <= z)
}

The APIs are interoperable, so we're into ergonomics, interoperability, ease of implementation, etc.

[comex]

I think that ideally there should be a way to compile the invariants to regular code and check them as runtime asserts, whether with quickcheck or some new crate. Thus, if at all possible, the syntax should be a strict subset of Rust, even for things like quantifiers (which can be expressed using iterator methods).

[brendanzab]

Might be worth looking at Liquid Haskell as inspiration. They use do constraint solving with refinements for verification purposes. Dafny and Whiley are also interesting languages that use constraint solving, but are more geared towards imperative programming and use contracts for verification. Might also be interesting to check out Ada's SPARK variant.

Would be nice if the specification language make it easy to transition between levels of verification. For example, starting from example tests (ie. #[test]), to generative testing (eg. quickcheck or proptest), then to solvers (eg. Z3), and finally to proof systems (eg. Coq+Iris or Lean). Being able to say, export the solved properties from Z3 to a proof system would be neat!

[vakaras]

@asajeffrey

I'm just wondering if there's some way we can specify the properties that are being verified in a way which is amenable to lots of different verification strategies.

I agree that we should aim for this when designing the specification language.

Regarding the Quickcheck, from the examples it seems that it is a way to specify the behaviour “externally” (could be even in a different file) while preconditions and postconditions is a way to specify the behaviour “inline”. In other words, we should agree if we want to support “external” or “inline” specifications. I am clearly biased here, but I think that the specification of an imperative function should be part of its signature and, therefore, I would prefer preconditions and postconditions written as function annotations.

@comex

I think that ideally there should be a way to compile the invariants to regular code and check them as runtime asserts, whether with quickcheck or some new crate.

This was the main reason why I proposed to have a distinction between basic assertions and tool specific assertions. My idea was that the basic assertions would be essentially boolean Rust expressions that are checked when the program is executed (either always, or in only debug builds). In other words, the function:

#[ensures="result >= a && result >= b"]
fn max(a: i32, b: i32) -> i32 {
    if (a < b) { b } else { a }
}

when compiled would become equivalent to:

fn max(a: i32, b: i32) -> i32 {
    let result = if (a < b) { b } else { a };
    assert(result >= a && result >= b, "The postcondition “result >= a && result >= b” failed.");
    result
}

Thus, if at all possible, the syntax should be a strict subset of Rust, even for things like quantifiers (which can be expressed using iterator methods).

I would suggest not to have quantifiers as part of basic assertions at least in the initial version because designing a single syntax of quantifiers that can be supported by different approaches is hard if at all possible.

@brendanzab

Dafny and Whiley are also interesting languages that use constraint solving

Thanks, for sharing. I was not aware of Whiley.

Would be nice if the specification language make it easy to transition between levels of verification.

I agree. Just, I probably would not call them levels of verification. Maybe approaches would be a more suitable word? At least I would like to draw a distinction between what we try to achieve and how.

For example, since SPARK uses the Why3 infrastructure, it supports using both SMT solvers (Z3, CVC4) and proof assistants (Coq, Isabelle) as back-end provers. So, if Z3 is not able to proof something automatically, you can switch to Coq and prove that “manually”. However, the properties you try to prove about your code in both cases are specified in SPARK and are independent of what prover you use.

I think the levels of verification would be more something like (I have adapted from a Yannick Moy's presentation about SPARK):

1. Manual bug finding (approach: manually writing tests).
2. Automatic bug finding (approaches: Quickcheck, proptest, fuzzers, concolic execution, model checking, lints).
3. Proving absence of runtime errors (approaches: static analysis, deductive verifiers such as Why3, SAW, and Viper).
4. Proving preservation of key properties such as termination, deadlock freedom, secure information flow, etc. (approaches: static analysis, deductive verifiers).
5. Proving full functional correctness (deductive verifiers, proof assistants such as Coq and Isabelle).

I think it would be nice to support smooth transitions between both approaches and levels.

By the way, as far as I know using Coq or Isabelle as a prover for SPARK requires to know the entire stack (SPARK + Why3) inside-out and is essentially doable only by the SPARK developers. Therefore, I think that Dafny or Liquid Haskell way where a programmer can guide the automatic prover by using some form of ghost code would be more approachable for programmers without strong verification background.

[asajeffrey]

Yes, the question of inline vs external specs is a tricky one. FWIW, in Rust, tests are separate from code, although possibly in the same file. Proof hints (e.g. loop invariants) pretty much have to be inline, but I don't think we're planning to standardize those soon.

[vakaras]

don't think we're planning to standardize those soon

What do you mean by “standardize”? That it would be available in stable Rust, or that several tools would use that? I am not sure whether it makes sense to try to stabilize any specification language before we have several tools successfully using it. In other words, until we have some confidence that it is actually usable. Does this make sense to you?

[denismerigoux]

I agree that the specification language we choose should be common to all the verification tools. This specification language should then make the distinction between pre/post-conditions and loop invariants, because this distinction is crucial for deductive verification frameworks (unlike Quickcheck).

However, I think that this specification language would require more than just boolean expressions. Indeed, for proving functional correctness one pattern is to prove a mapping between an optimized implementation and a pure model data structure.

For instance I am trying to prove the correctness of Servo's counting bloom filter. For that I need a ghost set of inserted elements (that could be expressed with PhantomData) which would be a functional-style data structure. This data structure would not necessarily need to be implemented in Rust, but rather be linked to a data structure supported by the proof tool. Ideally you should be able to call "pure" functions defined externally in your proof tool inside the Rust specification.

Also the specification language should include intermediate variable definitions, so that complex expressions can be defined (and readable). To keep things simple for the verification tool, the specification language should be completely pure, so the borrow-checker would not need to run on the specs (the lifetime should equal the scoping of the variable). Also quick syntax note : being able to give a name to the return type like the arguments should spare us a special result variable.

Concerning quantifiers, I do agree that their specification is too dependent on the proof tool being used and therefore should not be included in the spec language withing Rust.

What all these considerations lead to in my opinion is a two-staged specification language:

• the first stage would be a boolean-expression-based language, but that can define intermediate variables and call into "pure" functions returning a boolean. For instance:

fn is_greater(m:i32, a:i32, b:i32) -> bool {
   m >= a && m >= b
}

#[ensures="let max_ok = is_greater(m,a,b);max_ok"]
fn max(a: i32, b: i32) -> m:i32 {
    if (a < b) { b } else { a }
}

• the second stage would be extending this language to link external "pure" functions returning booleans and abstract types but that would be defined in the proof tools.

[fpoli]

To keep things simple for the verification tool, the specification language should be completely pure, so the borrow-checker would not need to run on the specs (the lifetime should equal the scoping of the variable).

I think that some checks should be run on the specification, to prevent the user from referring to borrowed locations like in the following example. The value of borrowed locations is not well-defined because other threads may be modifying it.

fn foo() {
    let mut x = T::new();
    let y: & _ = bar(&mut x);

    #[invariant="x.f > 0"]  // `x` should not be allowed here, `y` yes
    while ... { ... }

    baz(y);
    // y expires here
}

[leonardo-m]

Regarding the specifications we might want to write I suggest to copy from Why3:
http://why3.lri.fr/

Some usage examples:
http://toccata.lri.fr/gallery/why3.en.html

But that's not enough because Rust is impure and it doesn't have the several limitations given to Why3 to allow you to prove it. So some annotations from Ada-SPARK are needed to face the impure nature of Rust functions, I mean the SPARK annotations that specify how information flows in/out of a function beside the function arguments.

And that's not yet enough, you also have to allow only a subset of Rust features in those #[verify] functions (just like SPARK does with Ada), the idea is to implement things as how const functions are implemented in Rust: you start from allowing very little stuff inside a const function and then you iterate to add more and more stuff. The same should be done with Rust functions that are proved correct. And some Rust features will be unavailable into those proved functions for a very long time.