Function body annotations

Ghost commands

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

VeriFast preprocesses .rs files to replace annotations inside function bodies by dummy VeriFast_ghost_command(); statements. If an annotation inside a function body appears in a position where such a call is not allowed, you may get a confusing Rust compiler error.

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.