Formal Methods

(FYI: This is the doc for steering meeting compiler-team#498, "State of formal methods tools in Rust".)

The Goal

Rust is strongly positioned to make formal methods & verification mainstream in a way that hasn't been possible before. A combination of language design and community culture provide a unique opportunity, but we need to seize it. In this meeting I hope to bring up some of the concerns and difficulties that FM/FV developers have had with designing Rust tools and specifically rustc-based tools.

The "What"

Formal methods is a broad catch-all term which encompasses techniques ranging from typechecking, to model checking, to abstract interpretation, to deductive verification (and more). The underlying theme is the application of formal mathematical reasoning and tools to understand and extract information from programs. A formal methods tool is a (software) tool which applies one or more of these techniques to understand and guarantee properties of a program. Typically, they are written as compile-time tools: they run the program through a compilation pipeline and analyze the result.

Formal verification tools form a subset of formal methods concerned with techniques which enable proving a program satisfies a specification. These tools require a (formal) specification language, a language in which we can precisely describe the properties we want to guarantee of our programs. These languages are typically composed of a set of propositions (read: boolean expressions) and terms (read: pure expressions). Often they may look like normal programming languages but have several specific quirks: all terms and predicates must be terminating, they must all be pure (no side-effects) and they can often do "non-physical things" like constructing infinitely large values.

Rust specific context

Currently, the verification of Rust programs is a hot[^citation needed] topic in the academic research community (e.g. see this ACM search). This is largely due to Rust's strong, ownership type system which has been observed as greatly simplifying the difficulties of understanding and verifying the behavior of imperative programs.

Verifying the behavior of pointer programs is a well known hard program, in particular mutable aliasing causes all sorts of reasoning difficulties. The development of separation logic made the problem tractable but remains a heavy-weight tool to this day. Of course in Rust mutable references cannot alias at all; this restriction can dramatically simplify the work of verifying Rust programs.

The focus on safe abstractions of unsafe code also allows tools to pick and choose their battles: just like users tools can choose abstract away the implementation details, leaving the complex unsafe verification to other, specialized tools.

The "How"

The complexity and instability of the Rust language and ecosystem forces tools to rely on internal compiler APIs, which were not designed for them. This has pushed tools into a common architecture: implemented as a rustc driver which attempts to quickly place distance between itself and rust compiler apis by producing another IR, before finally generating target code. In many ways they can be seen as a form of codegen backend, but unlike standard Rust, these backends may be polymorphic, or may have different constraints from physical codegen.

As a starting point, most tools have settled on using MIR as the input language. This occurs for multiple reasons: MIR is drastically smaller than surface Rust, making it simpler to translate, it is better understood projects like RustBelt and MIRI help provide a solid basis for reasoning, and also it is where the borrow checker lives.

While this discussion will not cover the stability of MIR or its APIs, this issue is highly relevant to the underlying concerns of verification tools.

"Where" are the difficulties today?

Hopefully, the preceding introduction gives a little context and insight into the function and design of FM tools in Rust.

There is no expectation that t-compiler has a solution to any of these issues, they merely present challenges faced by FM developers today

Today, the challenges that FV tool developers face can be broadly be summarized in three key areas:

1. Integrating a specification language is difficult.

   This is the most cross-cutting issue: integrating a specification language requires hijacking the compiler, integrating a custom parser, type checker and codegeneration pathway in rustc, while interacting naturally with coherence, resolution, crates, etc.

   It almost works well, but several specific issues are highlighted below

2. Rustc APIS are limiting, lacking or too unstable for proper usage. In several key domains (ie: borrow checker, resolution) apis are unstable or lacking causign difficulties for tool developers.

3. Building tools which work well in a multi-crate environment is difficult currently. Rustc metadata is not extensible, and cargo is difficult to work with.

Specific issues are listed in the Appendix.

Future Work

Long term, many voices in the RFMIG wish to see Rust tools converge towards a shared platform for verification, which would allow different analyses to collaborate and communicate on proofs. This platform would encompass need to encompass a shared and 'blessed' specification language, and provide a stable-(ish) IR and APIs. It would also represent the ideal moment to decouple verification tools from internal compiler APIs by providing a facade.

I believe that addressing some of these issues helps lay the groundwork for this platform though the road ahead remains long.

Appendix

Issues are annotated with ***, **, * as a heuristic for importance.

Specification languages

Specification languages are a primordial feature of verification tools, but as it stands today, it can be quite challenging to 'integrate' a specification language into Rust. In many ways a specification language effectively extends the host language, and this is difficult to replicate with current rustc APIs.

The issues span from parsing, to typing, to 'lowering' specifications. Yet, Rust in many ways is almost there, a few nudges could provide a good platform for tools to build off of.

Adding new 'core' traits and types is very difficult ***

Verification tools essentially extend Rust by adding specification languages. Naturally, there can emerge a desire or requirement to add new traits or types which are fundamental to this specification language (think like Drop, Eq or Fn*). The way these kinds of traits and types are handled in Rustc makes it extremely difficult or impossible to do, even with API access.

As a simple example, we can consider Int the type of mathematical integers, there is no mechanism by which we can allow constants to refer to integer values (minor inconvenience).

For a more complex example, see below the issue about closure impls

No easy way to specify functions coming from std **

Giving specifications to standard libraries and types is an essential challenge for FM tools. While it is possible to define a custom wrapper of Vec and directly provide specifications, we cannot do the same for key traits like Index, Add or Eq.

Tools provide various hacks to add 'external specifications', it is highly brittle and leads to sub-par UX. The alternative is forking the entire stdlib, which is equally untractable for verification tools due to the speed of evolution and the manpower requirements.

Encoding specifications is brittle and leads to correctness worries ***

Tools may need to encode specifications (assertions, invariants) at specific points in a function, they often do this by inserting some marker expression which they can identify from MIR as the location of interest. This causes the generated MIR to potentially change, fairly dramatically from the unannotated code. For example in Creusot, we use a closure to mark and hold the specification at a specific point. This causes the MIR to include a bunch of irrelevant locals and assignments related to the closure.

An example, we have rust code like such:

#[invariant(condition)]
loop {
  ...
}

Here, invariant denotes a loop invariant condition. This invariant needs to somehow be encoded so that we can see it in the MIR. The common approach is an encoding like the following:

{ let _ = || { condition-encoding };}
loop {
  ...
}

Which generates MIR where a closure assignment will be performed before the loop blocks. By recognizing the closure, the verification tool can then correctly translate the condition. This is unsatisfactory for several reasons: it is highly vulnerable to compiler changes, the closure generation can also cause the MIR to generate many extra locals which don't really belong. This can complicate verification further down the line, as well as introduce fears that those extra variables (and different CFG) somehow change the behavior of the function.

A potential solution could be to add some 'Attribute' StatementKind which is a no-op operationally but works more cleanly with MIR and various optimizations and holds information needed to encode or identify specifications?

No easy way to create a 'custom namespace' for specifications *

As part of specification languages, it is desirable to offer the opportunity to declare custom 'functions' which are not Rust functions, they may only be used in specifications. As such, it would be desirable to seperate these in a custom namespace so that accidental calls generate a nice, helpful error message.

This can almost be achieved using Span::def_site() in a proc_macro but it seems like there may be a bug with the interaction with resolution.

Cargo & Multi-crate projects

Support for custom metadata in crates *

Because verification tools often are extending the compiler / language in certain ways, they need to track supplementary information about various DefId across crate boundaries. This requires building a custom version of the rustc_metadata system, which in turn does not play well with cargo as it has no knowledge of these custom metadata files. A solution would be to allow the crate metadata to contain a zone of opaque bytes which drivers can fill, or otherwise make the metadata format more flexible and extensible.

Custom cargo plugins have undesirable interaction with caching ***

When packaging a verification tool as a cargo plugin, there can be undesirable interactions with cargo's caching mechanism. Cargo caches invocations based on command line arguments but not environment varibles, however, when using RUSTC_WRAPPER to invoke a verification backend, it's necessary to pass your arguments in as environment variables, leading to invalid caching.

bjorn3 You can pass them in RUSTFLAGS and then have the RUSTC_WRAPPER filter out arguments for the verification backend. This is the approach miri takes. It works quite well. If you use the custom codegen backend infrastructure you can also pass it in -Cllvm-args. This is an opaque blob interpreted by the backend (originally meant for the llvm backend, but it can be any backend)

API difficulties

Incredibly difficult to recover expression for const_expr *

In the MIR APIs it's hard to recover a Rust expression which leads to a specific constant. It seems like the best we can do is ask for evaluation to bits or attempt to recover it from a promoted body.

bjorn3 The valtree initiative may help a bit with this.

Working with 'promoted bodies' is very awkward. *

Promoted bodies are painful to work with as they have no proper DefIds of their own, and are thus 'hard to name', they complexify the handling of constants.

bjorn3 You could name them as something like parent_defid__promoted_number.

The borrow checker apis are difficult to use and unstable **

Certain verification tools (especially Prusti[^1]) need access to the information and loans calculated by the borrow checker. Due to the WIP nature of polonius, it is difficult to extract this information, requiring fact files to be written to disk as an intermediate step.

No easy way to create definitions, types or impls within a plugin **

The rustc apis seemed to be designed in a 'read-only' manner, once parsing and resolution have been performed, there is no way to create 'synthetic' items. This causes issues when plugins attempt to mimic behaviors of the compiler for language items (ie: auto trait impls).

bjorn3 You can create items before HIR lowering. The HIR is meant to be immutable. Changing the HIR would require some way to invalidate all computed queries.

No way to provide custom implementations for closures *

In Rust closure types are opaque, the reasons for this are understandable in user-code, but for verification tools, we may need to give implementations to closures for custom traits. This is impossible as far as I can tell, neither through the apis nor code-generation can we give closures custom implementations.

To give a concrete example, imagine we wish to provide a trait FnOnceSpec which captures the specification of a callable expression using a predicate precondition:

trait FnOnceSpec {
  #[predicate] fn precondition(self) -> bool;
  ...
}

We wish to generate a custom instance for each individual closure, but today there is no mechanism through which this can be accomplished.

Resugaring spans *

It is hard to map source spans in MIR back to source level constructs (ie: resugaring a for-loop).

bjorn3 Source spans are the wrong level of abstraction I think. It is totally valid for rustc to use a dummy span for everything. Desugaring of for loops happens during HIR lowering.

Extending the set of available impls during trait resolution is hard (impossible?)

This is merely a generalization of the previous remark, it seems currently impossible to add 'builtin impls' for custom traits. As it stands, trait resolution special cases several traits and types, but does so in a closed-off manner.

Reverse span lookups *

It is hard to identify the expression which is found at a given span (HIR or otherwise).

Meeting Questions/Discussion Topics below Here