Introduction

VeriFast is a tool for modular formal verification of the absence of undefined behavior in Rust¹ programs that use unsafe blocks and the soundness of Rust modules that use unsafe blocks. It works by symbolically executing each function separately, using a separation logic representation of memory, starting from a symbolic state that represents an arbitrary program state that satisfies the function's precondition, and checking that each state at which the function returns satisfies the function's postcondition. By using the callee's precondition and postcondition instead of its body when symbolically executing a function call, and by using the user-specified loop invariant when symbolically executing a loop so as to be able to symbolically execute the loop body only once, and by using symbols to represent possibly infinitely many program states using a finite number of symbolic states, VeriFast covers all (usually infinitely many) possible executions of a function using a finite (and usually small) number of symbolic executions, allowing the verification of (small) programs to usually complete in a matter of seconds.

For functions not declared as unsafe, VeriFast derives a precondition and postcondition from the function's parameter types and return type using the separation logic interpretation of Rust's types defined by RustBelt; for functions declared as unsafe, the user has to provide a precondition and postcondition by inserting specially marked comments called annotations into the source code. Similarly, for each loop a loop invariant has to be provided in an annotation. To be able to express these conditions (called assertions), the user may generally also have to insert annotations defining mathematical recursive datatypes called inductive datatypes, mathematical recursive functions over these datatypes called fixpoint functions, recursive named separation logic assertions called predicates, and type predicates defining a custom interpretation for some of the struct types defined by the current module (as well as some less common constructs such as VeriFast named function types, lemma function types, predicate families, and predicate family instances).

In order for symbolic execution to succeed, the user may furthermore have to insert annotations containing ghost commands such as open and close commands for unfolding and folding predicates and calls of lemma functions, possibly recursive functions defined inside annotations that are checked by VeriFast to terminate and to not have side-effects and that serve as possibly inductive proofs about fixpoint functions and predicates.

This reference defines the syntax of the various kinds of annotations, and describes VeriFast's symbolic execution algorithm and the various checks that VeriFast performs.

Soundness of VeriFast

We aim for VeriFast to be sound, i.e. that if VeriFast reports "0 errors found", then indeed each function not marked as unsafe in the crate under verification is semantically well-typed, which for parameterless non-unsafe functions like main implies that no execution of the function has undefined behavior. However, in contrast to some other tools such as RefinedRust, VeriFast itself has not been formally verified, so unknown bugs are almost certainly present in the tool that may cause the tool to report "0 errors found" incorrectly in some cases. There may also be known unsoundnesses; these should all be recorded as issues with label unsoundness. Also, when using command-line flags like -disable_overflow_check, -ignore_ref_creation, -allow_assume, and -ignore_unwind_paths, the soundness property can only be expected to hold under the assumption that the program does not perform arithmetic overflow, complies with the pointer aliasing rules, does not violate any of the assume ghost commands present in the program, and does not violate semantic well-typedness due to unwinding, respectively. Finally, note that since VeriFast for Rust uses the rustc frontend, which assumes a particular compilation target architecture and particular configuration options (such as debug_assertions), VeriFast for Rust's result will only hold for the current target architecture and configuration options.

The state of VeriFast

VeriFast has been developed by Bart Jacobs, Jan Smans, and Frank Piessens at KU Leuven, Department of Computer Science, DistriNet research group since 2008, with many contributions from contributors inside and outside DistriNet. VeriFast for Rust has been developed by Nima Rahimi Foroushaani and Bart Jacobs at DistriNet since 2022. The lead developer and main maintainer is Bart Jacobs, an associate professor at DistriNet, who combines these activities with his usual research, education, and service duties. The largest verification performed so far with VeriFast for Rust, the verification of certain properties of certain functions of the Rust standard library's LinkedList data structure, was performed in December 2024. Its support for the Rust language is as of yet very incomplete², so that for any new nontrivial use case, it is to be expected, for now, that the tool will have to be extended. Bart Jacobs is eager to support anyone interested in using VeriFast. However, despite his best intentions, he may get distracted by other occupations; in that case, please do not hesitate to remind him early and often---your continued showing of interest will only delight him and you may rest assured that, given sufficient prodding, your issue will be resolved eventually.

The state of this reference

This reference is under construction; much material is still missing. Please bear with us! But if there are particular parts you're particularly eager to see, it always helps to let us know.

Further resources

There is a brief introduction to VeriFast for Rust, with a few examples, in the Verify Rust Std Lib book.

A tutorial is being prepared. In the meantime, the VeriFast Tutorial for C is a good resource for familiarizing yourself with VeriFast's concepts. Rust versions of the examples and exercises of the VeriFast Tutorial are available; see the command lines used to verify them in verify.mysh (where they are listed in the order in which they appear in the Tutorial). (Note: the solutions found there can be transformed into starting points for exercises by stripping the VeriFast annotations using bin/vfstrip: e.g. vfstrip < account.rs > account_stripped.rs.)

Further examples of VeriFast for Rust proofs are in tests/rust; the command lines are in tests/rust/testsuite.mysh.

Symbolic execution states

A symbolic execution state consists of the following components:

• A symbolic store, mapping each local variable name in scope whose address is not taken to a term representing its current value, and each local variable in scope whose address is taken to a term representing a pointer to the variable.
• A symbolic heap, a multiset of heap chunks representing the resources owned by the code being verified. Note: "symbolic heap" and "heap chunk" are slightly misleading names, because ownership of non-heap resources, such as global variables or stack-allocated variables whose address is taken¹, is also represented as "heap chunks"; more accurate names would have been "symbolic multiset of owned resources" and "chunk of resource".
• A path condition, a set of formulae (terms of type bool) encoding the assumptions made about the symbols used on the current symbolic execution path.

These components are shown in the Locals pane, the Heap chunks pane, and the Assumptions pane of the VeriFast IDE, respectively.

A heap chunk consists of the following components:

• The chunk's coefficient: a term representing a real number. In case of an application of a built-in predicate representing a region of memory, the coefficient is always greater than zero and not greater than one. If the coefficient equals one, it's a full chunk denoting read/write access; otherwise, it's a fractional chunk denoting read-only access. In case of a user-defined predicate, the meaning is given by distributing the multiplication by the coefficient over the separating conjunctions in the predicate's body. If a chunk's coefficient is the literal term 1, it is not shown in the VeriFast IDE.
• The chunk's predicate: a term representing a predicate value. When processing a predicate definition, VeriFast allocates a fresh predicate symbol to represent the predicate; also, each predicate constructor is associated with a function symbol mapping a predicate constructor argument list to a predicate value.
• The chunk's type arguments, a list of types with which to instantiate the predicate's type parameters.
• The chunk's arguments, a list of terms with which to instantiate the predicate's parameters.
• Optionally, the chunk's size. This is only potentially present when verifying a lemma function whose precondition's first separating conjunct is a predicate assertion. In that context, chunks derived from the first chunk produced by the lemma function's precondition through N open operations have size -N. This component is used to verify termination of lemma functions defined by induction on the derivation of the precondition's first chunk.

A predicate is either built-in or user-defined. All built-in predicates are declared in the prelude, in bin/rust/prelude.rsspec, or are automatically generated by VeriFast when it processes certain declarations. The most important ones are the following:

• pred points_to_<T>(p: *T, v: option<T>): a chunk points_to_::<T>(p, v) denotes ownership of a variable of type T pointed to by properly aligned pointer p. If v is some(V), the variable is initialized and holds value V; otherwise, it is uninitialized. Since the points-to chunk for a variable is consumed when the variable is deallocated, ownership of a points-to chunk implies that the pointer is non-dangling.
• pred points_to<T>(p: *T, v: T): equivalent to points_to_::<T>(p, some(v)).
• pred array_<T>(p: *T, n: i32, vs: list<option<T>>): a chunk array_::<T>(p, n, vs) denotes ownership of an array of n components of type T, pointed to by properly aligned pointer p. List vs of length n holds each component's value, if it is initialized, or none if it is not.
• pred array<T>(p: *T, n: i32, vs: list<T>): denotes ownership of a fully initialized array.
• When processing a definition of a struct S with fields F1: T1 through Fn: Tn, VeriFast introduces field predicates pred S_F1_(p: *S, v: option<T1>) = points_to_::<T1>(&(*p).F1, v) and pred S_F1(p: *S, v: T1) = points_to::<T>(&(*p).F1, v) through S_Fn_ and S_Fn, as well as a padding predicate pred struct_S_padding(p: *S).

Annotations

This chapter defines the syntax and the semantics of the various contructs that may appear inside VeriFast annotations.

• Keywords
• Types
• Expressions
• Assertions
• Function specifications
• Function body annotations
  • Ghost commands
  • Block annotations
  • Call annotations
• Ghost declarations

Keywords

In annotations, these words, in addition to Rust's keywords, are recognized as keywords and cannot be used as identifiers:

_ above abstract_type activating action and_fresh_handle
and_handle any assert assume_correct below box_class by close
consuming_box_pred consuming_handle_pred copred create_box
create_fresh_handle create_handle decreases dispose_box
dup_lem_ptr_chunk emp ens extends fix fix_auto fn_type
forall_ handle handle_pred import_module inductive inv leak
lem lem_auto lem_type let_lft merge_fractions
nonghost_callers_only on_unwind_ens open perform_action permbased pred
pred_ctor pred_fam pred_fam_inst preserved_by produce_fn_ptr_chunk
produce_lem_ptr_chunk producing_box_pred producing_fresh_handle_pred
producing_handle_pred req require_module split_fraction terminates
truncating type_pred_decl type_pred_def typedef typeid
unloadable_module

These are the additional operators recognized inside annotations:

&*& |-> |-?-> @

Types

Inside annotations, the syntax of types is extended as follows:

^Syntax
Type :
      ... | *_ | any | PureFunctionType | PredicateType | real

PureFunctionType :
      fix ( ( ParamType , )^* ParamType^? )

ParamType :
      (IDENTIFIER :)^? Type

PredicateType :
      pred ( ((( ParamType , ) ParamType )^? ; )^? ( ParamType , ) ParamType^? )

In addition to (some subset of) Rust's types, VeriFast supports the following types:

• Type *_ (pointer-to-anything) is a pointer type implicitly convertible to any other pointer type. It is analogous to C's void *.
• Type any is the union of all inductive types that themselves contain any only in positive positions.
• The pure function type fix(T1, ..., Tn, U) is the type of mathematical functions taking N arguments, of types T1 through Tn, and returning a value of type U.
• The predicate type pred(T1, ..., Tn) is the type of separation logic predicates taking N arguments, of types T1 through Tn. The type pred(T1, ..., Tn; U1, ..., Um) is the type of precise separation logic predicates taking N input arguments and M output arguments.
• Type real is the type of real numbers. (It is mostly used for chunk coefficients and for reasoning about floating-point numbers.)

In pure function types and predicate types, parameter names may optionally be written for documentation purposes; they are ignored by VeriFast.

Note, furthermore:

• VeriFast does not distinguish between *const T and *mut T and supports the syntax *T. That is, VeriFast treats the type expressions *const T, *mut T, and *T identically.
• When used as the type of a ghost variable (e.g. a pure function parameter or return value, a predicate parameter, a lemma parameter, or a ghost cell) or as the type of an expression in an annotation, all integer types are interpreted as the mathematical type ℤ of all integers. Also, inside annotations arithmetic operations on integers are always interpreted as operations on ℤ and never wrap around.

Expressions

^Syntax
Expression : ... | Lifetime | typeid ( Type )

The syntax of expressions in annotations is the same as in Rust code, with two additional supported forms:

• A lifetime parameter in scope may be used as an expression. This denotes the RustBelt lifetime_t value corresponding to that lifetime parameter.
• The expression typeid(T) denotes the typeid of type T.

Also, certain Rust expressions are interpreted differently in annotations than in Rust code:

• Array expressions are interpreted as list<T> values. For example, [10, 20, 30] is interpreted as cons(10, cons(20, cons(30, nil))).
• Arithmetic expressions on integer types are interpreted as operations on the mathematical set ℤ of all integers; they produce their mathematical result and never wrap around.

Note that match expressions may be used to perform case analysis on values of VeriFast inductive types.

Assertions

^Syntax
Assertion :
      PointsToAssertion
   | PredicateAssertion
   | TypePredicateAssertion
   | BooleanAssertion
   | PatternMatchingEqualityAssertion
   | ConditionalAssertion
   | MatchAssertion
   | Assertion &*& Assertion

PointsToAssertion : ( [ VFPattern ] )^? Expression ( |-> | |-?-> ) VFPattern

VFPattern : _ | ? ( IDENTIFIER | _ ) | Expression

PredicateAssertion : ( [ VFPattern ] )^? Expression VFPatternList ^? VFPatternList

VFPatternList : ( (( VFPattern , )^* VFPattern )^? )

TypePredicateAssertion : < Type > . IDENTIFIER VFPatternList

BooleanAssertion : Expression

PatternMatchingEqualityAssertion : Expression == VFPattern

ConditionalAssertion : if Expression { Assertion } else { Assertion }

MatchAssertion : match Scrutinee { ( MatchAssertionArm ,^? )^* }

MatchAssertionArm : Pattern => Assertion

Function specifications

VeriFast accepts the following specification clauses between a function's header and its body:

^Syntax
SpecificationClause :
      /*@ req Assertion ; @*/
   | /*@ ens Assertion ; @*/
   | /*@ on_unwind_ens Assertion ; @*/
   | /*@ assume_correct @*/

Note that VeriFast also support single-line annotations of the form //@ ...annotation.... Such an annotation is entirely equivalent to /*@ ...annotation... @*/.

Notice that the requires clause, the ensures clause, and the unwind ensures clause must be in separate annotations.

Function body annotations

Ghost commands

VeriFast accepts the following ghost commands as annotations in positions where statements are allowed in Rust code.

^Syntax
GhostCommandAnnotation : /*@ GhostCommand @*/

GhostCommand :
      open PredicateAssertion ;
   | close PredicateAssertion ;
   | let IDENTIFIER = Expression ;
   | if Expression { GhostCommand ^* } ( else { GhostCommand ^* } )^?
   | match Scrutinee { MatchGhostCommandArm ^* }
   | assert Assertion ;
   | leak Assertion ;
   | produce_lem_ptr_chunk TypePath ( (( Expression , )^* Expression )^? ) ( (( IDENTIFIER , ) IDENTIFIER )^? ) { GhostCommand ^* } ( ; | { GhostCommand ^* } )
   | produce_fun_ptr_chunk TypePath ( Expression ) ( (( Expression , )^* Expression )^? ) ( (( IDENTIFIER , ) IDENTIFIER )^? ) { GhostCommand ^* }
   | { GhostDeclaration ^* GhostCommand ^* }
   | return Expression ^? ;
   | Expression ;

A return ghost command may only appear in a lemma body, not in a ghost command annotation.

Block annotations

Additionally, a Rust block may start with one of the following VeriFast annotations:

• a loop invariant of the form /*@ inv Assertion ; @*/
• a loop specification of the form /*@ req Assertion ; ens Assertion ; @*/. Notice that here, the requires clause and the ensures clause must be in the same annotation, whereas in the case of function specifications they must be in separate annotations.
• a batch of ghost declarations of the form /*@ GhostDeclaration ^* @*/ The declarations supported in such batches are predicate definitions, lemma definitions, and local lifetime variable definitions (using let_lft).

Call annotations

Furthermore, a ghost generic argument list annotation may be inserted between the function name and the argument list of a Rust function call, like so: foo/*@::<'a, T>@*/. This is necessary in cases where it is important to pass a particular lifetime as a generic argument to a function. If, for a function call, no ghost generic argument list is provided, VeriFast uses 'static as the argument for each of the function's lifetime parameters.

Ghost declarations

A ghost declarations annotation may appear anywhere a Rust item may appear, except that only a few kinds of ghost declarations are supported inside function bodies (see Block annotations).

^Syntax
GhostDeclarationsAnnotation : /*@ GhostDeclaration ^* @*/

GhostDeclaration :
      pub GhostDeclaration
   | inductive IDENTIFIER GenericParams ^? = |^? InductiveConstructor ( | InductiveConstructor )^* ;
   | fix IDENTIFIER GenericParams ^? ( Params ) ( -> Type )^? ( { Expression } | ; )
   | pred IDENTIFIER GenericParams ^? ( ( Params ; )^? Params ) ( = Assertion )^? ;
   | pred_ctor IDENTIFIER GenericParams ^? ( Params ) ( ( Params ; )^? Params ) = Assertion ;
   | pred GenericParams ^? < Type > . IDENTIFIER ( ( ParamNames ; )^? ParamNames ) = Assertion ;
   | lem IDENTIFIER GenericParams ^? ( Params ) ( -> Type )^? LemmaRest
   | fn_type IDENTIFIER GenericParams ^? ( Params ) = unsafe fn ( Params ) ( -> Type )^? ; req Assertion ; ens Assertion ; on_unwind_ens Assertion ;
   | lem_type IDENTIFIER GenericParams ^? ( Params ) = lem ( Params ) ( -> Type )^? ; req Assertion ; ens Assertion ;
   | let_lft Lifetime = Expression ;
   | abstract_type IDENTIFIER ;

InductiveConstructor : IDENTIFIER ( ( ( ParamType , )^* ParamType ) )^?

LemmaRest :
      LemmaSpecification { GhostCommand ^* }
   | ; LemmaSpecification

LemmaSpecification : nonghost_callers_only^? req Assertion ; ens Assertion ;

Params : (( Param , )^* Param )^?

Param : IDENTIFIER : Type

ParamNames : (( IDENTIFIER , )^* IDENTIFIER )^?

Verifying compliance with Rust's pointer aliasing rules

Breaking Rust's pointer aliasing rules or mutating immutable bytes is undefined behavior. VeriFast currently verifies (only) the latter.

In particular, it verifies that the memory pointed to by a shared reference, except for the memory inside an UnsafeCell, is not mutated while the shared reference is active. First of all, shared reference creation is treated like the creation of a new pointer value, with the same address but a different provenance from the original pointer. Points-to resources for the original pointer cannot be used for accesses through the new shared reference.

VeriFast requires, at creation of a shared reference, that the user transfer a fraction greater than 0 and less than 1 of the points-to resources for the original place to the new shared reference. These resources are transferred back to the original reference when the shared reference is ended (and only then); from that point on, the shared reference is no longer usable.

Specifically, a shared reference creation expression &E is treated like a call of function create_ref in aliasing.rsspec, which is part of the VeriFast for Rust prelude. This function requires that a shared reference value has been precreated using lemma precreate_ref declared in the same file. Furthermore, it requires that the new reference has been initialized.

Memory inside an UnsafeCell is exempted from this process; the points-to resources for that memory are never transferred. This means that a shared reference to an UnsafeCell does not directly provide access to the memory behind the UnsafeCell. To access the memory, the developer has to call UnsafeCell::get. VeriFast treats calls of this method like calls of logical function ref_origin (also declared in aliasing.rsspec). Therefore, if a struct S has a field f of type UnsafeCell<T> inside, it is important for <S>.share(k, t, l) to (directly or indirectly, e.g. via a nonatomic borrow), assert points-to resources for ref_origin(&(*l).f). See, for example, cell.rs and mutex.rs.

Verifying non-unsafe functions

RustBelt

A core value proposition of Rust is that well-typed programs have no undefined behavior, under certain conditions on the use of unsafe blocks. The RustBelt project has developed a mathematically precise proposal for what those conditions are. In this proposal, a semantics is defined for Rust's types and typing judgments in separation logic, providing a definition of whether a function is semantically well-typed that talks only about the function's behavior, not about its precise syntactic structure, and is therefore applicable to functions containing unsafe blocks. They have proven the soundness of Rust's type checker with respect to this semantics, implying that if a function that does not contain unsafe blocks is syntactically well-typed, then it is semantically well-typed. Therefore, if a program consists of modules that use unsafe blocks and client code that does not, it suffices to establish that these modules are semantically well-typed to be able to conclude that the program as a whole is semantically well-typed and therefore has no undefined behavior.¹

In order to be able to express the semantics of mutable references and shared references, as well as the semantics of many of the uses of interior mutability in the Rust standard library, the RustBelt authors have proposed the lifetime logic, which defines separation logic concepts such as lifetime tokens, full borrows, fractured borrows, thread tokens, and nonatomic borrows.

An excellent resource for learning more about the RustBelt proposal and the advanced separation logic Iris that underlies it is Ralf Jung's thesis.

RustBelt and the lifetime logic in VeriFast

An axiomatisation of the lifetime logic into VeriFast's logic and some further RustBelt-related definitions and axioms can be found in the following files:

• bin/rust/rust_belt/lifetime_logic.rsspec
• bin/rust/rust_belt/general.rsspec

A brief tutorial introducing VeriFast's encoding of the lifetime logic is available.

Semantic well-typedness of functions in VeriFast

If a crate under verification defines a function not marked as unsafe, VeriFast generates a specification for that function that expresses the function's semantic well-typedness. If the function is annotated with an explicit specification as well, VeriFast first verifies that the explicit specification implies² the generated one, and then verifies the function body against the explicit specification; otherwise, VeriFast verifies the function body against the generated specification.

For a function fn f<'a, 'b : 'a, T, U>(x1: T1, ..., xN: TN) -> U, the generated specification is as follows:

req thread_token(?_t) &*&
    [?_q_a]lifetime_token('a) &*&
    [?_q_b]lifetime_token('b) &*& 
    lifetime_inclusion('a, 'b) == true &*&
    <T1>.own(_t, x1) &*&
    ...
    <TN>.own(_t, xN);
ens thread_token(_t) &*&
    [_q_a]lifetime_token('a) &*&
    [_q_b]lifetime_token('b) &*&
    <U>.own(_t, result);
on_unwind_ens
    thread_token(_t) &*&
    [_q_a]lifetime_token('a) &*&
    [_q_b]lifetime_token('b);

Drop functions

If the crate under verification implements Drop for a struct S<'a> with fields f1 : T1 through fN : TN, VeriFast generates the following specification for drop(&mut self):

req thread_token(?_t) &*&
    [?_q_a]lifetime_token('a) &*&
    <S>.full_borrow_content(_t, self);
ens thread_token(_t) &*&
    [_q_a]lifetime_token('a) &*&
    <T1>.full_borrow_content(_t, &(*self).f1) &*&
    ...
    <TN>.full_borrow_content(_t, &(*self).fN);
on_unwind_ens
    thread_token(_t) &*&
    [_q_a]lifetime_token('a) &*&
    <T1>.full_borrow_content(_t, &(*self).f1) &*&
    ...
    <TN>.full_borrow_content(_t, &(*self).fN);

Semantics of types in VeriFast

For simple types T such as bool and the integer types, we simply have <T>.own(t, x) = true. Here are some more interesting cases:

• <&'a mut T>.own(t, l) = full_borrow('a, <T>.full_borrow_content(t, l))
• <&'a T>.own(t, l) = <T>.share('a, t, l)

For any type T, we have <T>.full_borrow_content(t, l) = *l |-> ?x &*& <T>.own(t, x).

For simple types T such as bool and the integer types, we simply have <T>.share(k, t, l) = frac_borrow(k, <T>.full_borrow_content(t, l)).

If the crate under verification defines a struct S, it can define a custom semantics for type S by defining the <S>.own and <S>.share predicates.³ If it does so, it must also prove a number of proof obligations about these predicates.

Proof obligations for own

If a crate defines a struct S as well as a custom definition of <S>.own, and the struct's field types are not trivially droppable and the struct does not implement the Drop trait, then the crate must prove the following lemma:

lem S_drop()
    req S_own(?t, ?s);
    ens <T1>.own(t, s.f1) &*& ... &*& <Tn>.own(t, s.fn);

where the fields of S are f1 through fn and their types are T1 through Tn.

If a crate defines a struct S as well as a custom definition of <S>.own, and S is Send, and the own predicate mentions the thread id, then the crate must prove the following lemma:

lem S_send(t1: thread_id_t)
    req S_own(?t, ?s);
    ens S_own(t1, s);

Proof obligations for share

If a crate defines a struct S as well as a custom definition of <S>.share, then the crate must prove the following two lemmas:

lem S_share_full(k: lifetime_t, t: thread_id_t, l: *S)
    req atomic_mask(MaskTop) &*& [?q]lifetime_token(k) &*& full_borrow(k, S_full_borrow_content(t, l)) &*& ref_origin(l) == l;
    ens atomic_mask(MaskTop) &*& [q]lifetime_token(k) &*& [_]S_share(k, t, l);

lem S_share_mono(k: lifetime_t, k1: lifetime_t, t: thread_id_t, l: *S)
    req lifetime_inclusion(k1, k) == true &*& [_]S_share(k, t, l);
    ens [_]S_share(k1, t, l);

Additionally, if S is Sync and the share predicate mentions the thread id, then the crate must prove the following lemma:

lem S_sync(t1: thread_id_t)
    req [_]S_share(?k, ?t, ?l);
    ens [_]S_share(k, t1, l);

Generic structs

If struct S is generic in type parameters T1 through Tm, each of the above lemmas must also be generic in the same parameters. Furthermore, they may additionally require and ensure type_interp::<Ti>(), for each i. Furthermore, if a type parameter is Send or Sync, an is_Send(typeid(Ti)) == true or is_Sync(typeid(Ti)) == true conjunct may be added to the precondition. For example:

lem Pair_send<A, B>(t1: thread_id_t)
    req type_interp::<A>() &*& type_interp::<B>() &*& Pair_own::<A, B>(?t, ?pair) &*& is_Send(typeid(A)) && is_Send(typeid(B));
    ens type_interp::<A>() &*& type_interp::<B>() &*& Pair_own::<A, B>(t1, pair);
{
    open Pair_own::<A, B>(t, pair);
    Send::send::<A>(t, t1, pair.fst);
    Send::send::<B>(t, t1, pair.snd);
    close Pair_own::<A, B>(t1, pair);
}

The lifetime logic

Here, we introduce our encoding into VeriFast of Jung et al.'s lifetime logic, a library of separation logic constructs for expressing what it means in separation logic to own a mutable reference or a shared reference. More specifically, it enables defining a separation logic predicate <T>.own for each Rust type T such that <T>.own(v) expresses ownership of Rust value v of type T and such that a separation logic specification expressing semantic well-typedness of a Rust function f can be written as follows:

#![allow(unused)]
fn main() {
fn f(p1: T1, p2: T2) -> U
//@ req <T1>.own(p1) &*& <T2>.own(p2);
//@ ens <U>.own(result);
}

This specification expresses that the caller must pass ownership of argument values p1 and p2 into the function, and that the function must pass ownership of the return value to the caller when it returns. In other words, it expresses that the function is allowed to consume ownership of the argument values and is required to produce ownership of the result value.

(Note: for now, we ignore the fact that some Rust values (of non-Send types) are accessible only to particular threads.)

Mutable references

Consider the following example program:

fn increment(r: &mut i32) { *r += 1; }

fn main() {
    let x = 83;
    increment(&mut x);
    x /= 2;
    println!("The answer is {}", x);
}

We can verify safety of this program in VeriFast trivially as follows:

fn increment(r: &mut i32)
//@ req *r |-> ?v0;
//@ ens *r |-> ?v1;
{ *r += 1; }

fn main()
//@ req true;
//@ ens true;
{
    let x = 83;
    increment(&mut x);
    x /= 2;
    println!("The answer is {}", x);
}

The specification for increment requires that the caller pass exclusive ownership of the place referred to by r into the function, and requires the function to pass it back to the caller when it returns.

Notice, however, that this specification is not of the form that we are looking for: we are looking for a definition for <&mut i32>.own such that the specification for increment can be written roughly as

#![allow(unused)]
fn main() {
fn increment(r: &mut i32)
//@ req <&mut i32>.own(r);
//@ ens true;
}

That is, it should be sufficient for the caller to pass ownership of the mutable reference into the function, without the function passing any resources related to r back to the caller! But if the function cannot pass anything back, how can the caller get the permissions it needs to perform x /= 2;?

To solve this conundrum, it is crucial to remember that Rust associates a lifetime with each mutable reference. The full type of function increment is as follows:

#![allow(unused)]
fn main() {
fn increment<'a>(r: &'a mut i32)
}

The mutable reference is valid only until the end of lifetime 'a. Only after 'a has ended, can the caller again mutate the place. So ownership of a mutable reference should express the exclusive ownership of the place referred to by the reference, but only until the end of the associated lifetime.

This is exactly what is expressed by lifetime logic predicate full_borrow: full_borrow(k, p) expresses exclusive ownership of the resources described by predicate value p, but only until the end of lifetime k. We therefore define <&'a mut T>.own(l) = full_borrow('a, <T>.full_borrow_content(l)) where <T>.full_borrow_content is a predicate constructor that, when applied to argument list (l), constructs a predicate value <T>.full_borrow_content(l). Applying this predicate value to an empty argument list, in turn, asserts ownership of the place referred to by l, as well as ownership of the value stored at that place: <T>.full_borrow_content(l)() = *l |-> ?v &*& <T>.own(v).

We obtain the following specification for increment:

#![allow(unused)]
fn main() {
fn increment<'a>(r: &'a mut i32)
//@ req [?qa]lifetime_token('a) &*& <&'a mut i32>.own(r);
//@ ens [qa]lifetime_token('a);
}

The assertion [qa]lifetime_token('a) asserts fractional ownership of the lifetime token for lifetime 'a. The coefficient qa is a real number greater than 0 and not greater than 1. Starting a lifetime creates the lifetime token for that lifetime, and ending the lifetime destroys the token. Therefore, fractional ownership of the lifetime token for a lifetime guarantees that the lifetime is alive (i.e. that it has started and has not yet ended). The notation ?qa binds the coefficient to logical variable qa; the specification requires that the caller pass a fraction of the lifetime token for 'a to the function, and that the function pass the same fraction back to the caller when it returns.

Given this specification, we can verify function increment as follows:

#![allow(unused)]
fn main() {
fn increment<'a>(r: &'a mut i32)
//@ req [?qa]lifetime_token('a) &*& full_borrow('a, <i32>.full_borrow_content(r));
//@ ens [qa]lifetime_token('a);
{
    //@ open_full_borrow(qa, 'a, <i32>.full_borrow_content(r));
    //@ open <i32>.full_borrow_content(r)();
    *r += 1;
    //@ close <i32>.full_borrow_content(r)();
    //@ close_full_borrow(<i32>.full_borrow_content(r));
    //@ leak full_borrow('a, <i32>.full_borrow_content(r));
}
}

The proof uses lemma open_full_borrow. open_full_borrow(q, k, p) consumes full_borrow(k, p) and [q]lifetime_token(k) and produces p() as well as close_full_borrow_token(p, q, k). The latter can later be passed to lemma close_full_borrow to recover the lifetime token fraction [qa]lifetime_token(k). close_full_borrow(k, p) consumes close_full_borrow_token(p, q, k) and p(), for some q, and produces [q]lifetime_token(k). After closing the full borrow, the proof can leak it, since it is no longer needed.

The main function can then be verified as follows:

fn main()
//@ req true;
//@ ens true;
{
    let mut x = 83;
    //@ let k = begin_lifetime();
    //@ close <i32>.full_borrow_content(&x)();
    //@ borrow(k, <i32>.full_borrow_content(&x));
    {
        //@ let_lft 'a = k;
        increment/*@::<'a>@*/(&mut x);
    }
    //@ end_lifetime(k);
    //@ borrow_end(k, <i32>.full_borrow_content(&x));
    //@ open <i32>.full_borrow_content(&x)();
    x /= 2;
    println!("The answer is {}", x);
}

The proof starts a lifetime k, obtaining [1]lifetime_token(k). It then creates a full borrow of &x at k and binds semantic lifetime k to type system lifetime variable 'a using a let_lft declaration, so that it can call increment with lifetime generic parameter 'a bound to lifetime variable 'a. After the call returns, the proof can end the lifetime using lemma end_lifetime, which produces [_]lifetime_dead_token(k). That token can be used to end the full borrow with borrow_end and recover exclusive ownership of x.

Shared references

Now, consider the following example program:

fn add(r1: &i32, r2: &i32) -> i32 { *r1 + *r2 }
fn double(r: &i32) { add(r, r) }
fn main() {
    let mut x = 42;
    x = double(&x);
    x /= 2;
    println!("The answer is {}", x);
}

We can trivially verify this program as follows:

fn add(r1: &i32, r2: &i32) -> i32
//@ req [?f1](*r1 |-> ?v1) &*& [?f2](*r2 |-> ?v2);
//@ ens [f1](*r1 |-> v1) &*& [f2](*r2 |-> v2);
{ *r1 + *r2 }

fn double(r: &i32)
//@ req [?f](*r |-> ?v);
//@ ens [f](*r |-> v);
{ add(r, r) }

fn main()
//@ req true;
//@ ens true;
{
    let mut x = 42;
    x = double(&x);
    x /= 2;
    println!("The answer is {}", x);
}

The specification for function double requires the caller to pass it fractional ownership with coefficient f of the place at r, and requires the function to pass it back when it returns. The specification for add is similar.

Again, however, these specifications are not of the form that we are looking for: we are looking for specifications that express that ownership of the arguments is passed into the function, and ownership of the result is passed out when the function returns.

The question, then, is how to define <&i32>.own. Clearly, the definition must be different from that of <&mut i32>.own, since function double must be able to duplicate it and full borrows are not duplicable. Intuitively, <&i32>.own(l) should express shared ownership of place l and the value stored at that place. Usually, shared ownership in Rust means read-only ownership, but for types that have interior mutability, such as Cell and Mutex it can mean different things. Therefore, we use a separate per-type predicate <T>.share to express shared ownership: <T>.share(k, l) denotes shared ownership of the place of type T at l, and the value stored at that place, until the end of lifetime k. We define <&'a T>.own(l) = [_]<T>.share('a, l). The [_] prefix denotes that this is a dummy fraction that can be duplicated arbitrarily.

For types that do not involve interior mutability, such as i32, shared ownership should denote fractional ownership, but only until the end of the associated lifetime. To express this, the lifetime logic offers the frac_borrow predicate: ownership of a fractured borrow frac_borrow(k, p) allows the owner to obtain fractional ownership of the resources described by p, but only until the end of lifetime k. For types T that do not involve interior mutability, we define <T>.share(k, l) = [_]frac_borrow(k, <T>.full_borrow_content(l)). Using this definition, we can verify function add as follows:

#![allow(unused)]
fn main() {
fn add<'a>(r1: &'a i32, r2: &'a i32) -> i32
//@ req [?qa]lifetime_token('a) &*& [_]frac_borrow('a, i32_full_borrow_content(r1)) &*& [_]frac_borrow('a, i32_full_borrow_content(r2));
//@ ens [qa]lifetime_token('a);
{
    //@ let f1 = open_frac_borrow('a, i32_full_borrow_content(r1), qa/2);
    //@ let f2 = open_frac_borrow('a, i32_full_borrow_content(r2), qa/2);
    let result = *r1 + *r2;
    //@ close_frac_borrow(f1, i32_full_borrow_content(r1));
    //@ close_frac_borrow(f2, i32_full_borrow_content(r2));
    result
}
}

The proof obtains fractional ownership of the place at r1 by calling lemma open_frac_borrow: open_frac_borrow(k, p, q) consumes [_]frac_borrow(k, p) and [q]lifetime_token(k) and produces [f]p(), for some coefficient f which it returns as its return value, as well as a close_frac_borrow_token(f, p, q, k) which can later be passed to lemma close_frac_borrow to recover [q]lifetime_token(k).

The proof for double is trivial, because dummy fractions are duplicable:

#![allow(unused)]
fn main() {
fn double<'a>(r: &'a i32) -> i32
//@ req [?qa]lifetime_token('a) &*& [_]frac_borrow('a, i32_full_borrow_content(r));
//@ ens [qa]lifetime_token('a);
//@ safety_proof { assume(false); }
{
    add/*@::<'a>@*/(r, r)
}
}

The proof for main is as follows:

fn main()
//@ req true;
//@ ens true;
{
    let mut x = 42;
    //@ let k = begin_lifetime();
    //@ borrow(k, i32_full_borrow_content(&x));
    //@ full_borrow_into_frac(k, i32_full_borrow_content(&x));
    let result;
    {
        //@ let_lft 'a = k;
        result = double/*@::<'a>@*/(&x);
    }
    //@ end_lifetime(k);
    //@ borrow_end(k, i32_full_borrow_content(&x));
    x = result;
    x -= 42;
}

The proof creates a full borrow of x and then uses lemma full_borrow_into_frac to turn it into a fractured borrow.

Non-Send types and thread tokens

Above, we ignored the fact that some Rust values (of non-Send types), such as &Cell values and Rc values are accessible only to particular threads. To model this, each type's own predicate takes a thread identifier: <T>.own(t, v) asserts ownership of Rust value v of type T and that v is accessible to thread t. Similarly, <T>.share(k, t, l) asserts shared ownership of the place of type T at l and the value stored at that place, accessible to thread t, until the end of lifetime k.

Each function requires and ensures thread_token(t), providing access to resources accessible to thread t, where t denotes the current thread. The completed versions of the examples above are at full_borrow_tutorial.rs and frac_borrow_tutorial.rs.