Complete Vale syntax¶
This section presents a complete grammar for the Vale language. The grammar uses the following notation:
[ A ] indicates that A is optional.
A … A indicates that A is repeated zero or more times.
A [ … A ] indicates that A is repeated one or more times.
Variable/attribute/function/procedure/constructor/field/type/operator-type names are written as x, F, P, C, D, T, O, where:
F indicates a function name
P indicates a procedure name
C indicates a datatype constructor name
D indicates a datatype field name
T indicates a type name
O indicates an operator type name
For conciseness, the grammar omits attributes. Attributes are listed separately, in Attributes.
Grammar¶
Grammar |
Examples and notes |
|---|---|
|
|
|
|
|
type bool:Type(0) extern;
type my_bool:Type(0) := bool;
operand_type opr32:nat32 :=
| inout eax | inout ebx
| mem32 | const
var x:int;
const c:int extern;
function f(x:int, y:int):bool extern;
function f#[a:Type(0)](x:a):a extern;
procedure P(ghost x:int)
returns(ghost y:int)
requires
0 <= x;
isEven(x);
ensures
x <= y;
{ ... }
#verbatim
open FStar.Mul
#endverbatim
|
|
|
|
|
|
|
|
|
|
|
|
lets
x @= eax;
y @= ebx;
z := 3 + 3;
reads
x; y;
requires
x <= y < z;
let a := x + y;
is_even(a);
ensures
x == old(x);
let a := x + y;
is_even(a);
|
|
assume x < 10;
assert x <= 10;
assert x <= 10 implies p(x) by
{
myLemma(x);
}
forall (x:int, y:int)
x < y implies x <= y by
{
myLemma2(x, y);
}
// copy eax into immutable x:
let x := eax;
// let x be an alias for eax:
let x @= eax;
// mutable x:
ghost var x:uint32 := 33 + 44;
// ask solver to find an x:
let exists (x:int) 0 <= x;
reveal myOpaqueFunction;
reveal myOpaqueFunction(5, x);
Increment(x);
// declare x and y:
let (x:int, y) := MyProc(ebx, z);
// declare x and update y:
(let x:int), y := MyProc(ebx, z);
x := 5;
while (eax != 0)
invariant true;
decreases *;
{ ... }
if (eax != 5)
{
Increment(edx);
}
else
{
eax := 0;
}
|
|
calc ==
{
x;
==
x * 1;
== { myLemma(x); }
1 * x;
}
|
|
// these two lines are equivalent:
let (x:int, y) := MyProc();
(let x:int), (let y) := MyProc();
|
|
|
|
|
|
|
|
|
|
// 3.14159 is a real number
// bv1, bv2, etc. are bit vectors
// @x is the location of variable x
procedure P(in x:opr32)
requires
x == 10; // value in x
@x == OReg(Rax); // x's loc
{
}
function f#[a:Type(0)](x:a):a extern;
assert f(10) == 20; // Vale infers a
assert f#[int](10) == 20; // explicit
// cast x to type uint32
#uint32(x)
// cast x to type set(uint32)
#(set(uint32))(x)
// indexing and update
let s1:seq(int) := f();
let s2:seq(int) := s1[3 := "hi"];
assert s2[3] == "hi";
// assert that map m has key 10
assert m?[10];
old(x)
seq(10, 20, 30) // Dafny only
set(10, 20, 30) // Dafny only
list(10, 20, 30) // F* only
tuple(5, 15, true) // Dafny, F*
//binary operators:
// left-associative
// but ==> is right-associative
//
//highest precedence
/|\
| * / %
| + -
| < > <= >= is
| &&
| ||
| <== ==>
| <==>
\|/
//lowest precedence
let x := 3 in x + 1
forall(x:int, y:int){foo(x, y)}
foo(x, y) || x == y
|
|
|
|
|
|
uint32
map(int, set(uint32))
tuple(int, int, bool)
fun(int, int) -> bool
type byte:Type(0) :=
int_range(0, 0xff);
|
|
Verbatim blocks¶
Vale programs may contain verbatim blocks (VERBATIM_DECL_BLOCK in the table above):
#verbatim
method printCode(...) { ... }
lemma L(...) { ... }
#endverbatim
procedure P()
{
L(...);
...
}
#verbatim
method Main()
{
printHeader();
var n := printCode(va_code_P(), 0);
printFooter();
}
#endverbatim
Verbatim blocks are written as lines between #verbatim and #endverbatim.
Vale passes these lines directly to the verification language,
with no processing or analysis by Vale.
For example, verbatim blocks may be used to declare types, functions,
and lemmas in the underlying verification languages so that these
declarations may be used inside Vale procedures.
For FStar code, verbatim blocks can be written to the interface file (.fsti)
via #verbatim{:interface},
the implementation file (.fst)
via #verbatim or #verbatim{:implementation}
or both via #verbatim{:interface}{:implementation}.
Lexical structure¶
Single-line comments begin with //.
Longer comments can be placed in /* … */.
Comments can be nested inside each other: /* a /* b */ c */ is a valid comment.
Whitespace includes spaces, newlines, and carriage returns; tab characters are not allowed.
Variable names can include letters, _ characters, ' characters after the first character,
and digits after the first character.
There are special function names operator(+), operator(-), etc. to represent operators
in function declarations (see Functions and consts).
Vale programs can define new operator tokens
out of the characters
! % + - & ^ | < > = . # : $ ? ` ~ @ \ /
using the #token directive:
#token +. precedence +
#token declares a new token (+. in the example above)
that is parsed with the same precedence and associativity as an existing token
(+ in the example above).
This token can then be used for a custom operator, as described in Custom operators.
Attributes¶
Some elements of the Vale grammar may be annotated with attributes that supply additional information to Vale or to the verification language. Currently, attributes are only supported in the following places and on verbatim blocks:
Grammar (attributes) |
Examples and notes |
|---|---|
|
|
|
Attributes are not checked by Vale’s type checker, so they can contain arbitrary expressions.
Currently, the following attributes are supported:
on include directives:
{:from x}; filename is interpreted relative to the path alias x rather than to the current directory (see Modules and includes and Using the Vale tool)
{:verbatim} (Dafny only): include a file written directly in the underlying verification language, rather than including another Vale file
{:fstar} and {:open} (FStar only): include a file written directly in FStar, rather than including another Vale file, and, if {:open} is specified, open the declarations in the file into the Vale namespace
on procedures:
{:timeLimit n} and {:timeLimitMultiplier n} (Dafny only) set or increase the time limit for this procedure
{:options …} (FStar only) push-options/pop-options around procedure (examples:
{:options z3rlimit(20), max_ifuel(2)},{:options smtencoding.nl_arith_repr(boxwrap)},{:options using_facts_from("* -FStar.Seq.Base"), debug(FStar.Seq.Base)}){:restartProver} (FStar only) restart theorem prover to improve theorem prover predictability (
#restart-solverin FStar){:instruction EXP}, indicating a primitive procedure that is implemented with the code value specified by the expression EXP (see Instructions)
{:recursive} and {:decrease EXP}, indicating that a procedure may call itself, optionally specifying a decreases clause to prove the recursion’s termination
{:operand}, indicating an operand constructor
{:quick} (FStar only) – an experimental feature that uses a more complicated, but more efficient, FStar encoding for generated lemmas
on global variables:
{:state f(EXP, …, EXP)}, indicating that the variable x corresponds to a field f(EXP, …, EXP) of the state type.
on types:
{:primitive}, declaring a primitive type like
state,string, orlist
on verbatim blocks:
{:interface} and {:implementation} (FStar only) – see Verbatim blocks
Coding conventions¶
The following conventions are recommended (not required) for Vale programs:
Names
Names of non-ghost procedures (including instructions) start with an upper-case letter. Names of ghost procedures start with a lower-case letter. This helps to distinguish ghost and non-ghost procedure calls. Note that for FStar, ghost procedures must start with a lower-case letter; FStar will reject upper-case ghost procedure names.
Names of functions and constants may start with lower-case or upper-case letters, depending on the underlying verification framework conventions. FStar and Dafny typically use upper-case for datatype constructor functions and lower-case for other functions.
Names of types and global variables start with lower-case letters.
Names of operand types start with a lower-case letter, except for operand constructors, which start with an upper-case letter.
Names of type parameters and local variables should start with lower-case letters. In FStar, this is required.
Lower-case names use underscores to separate words:
my_name. Upper-case names may use underscores:MyNameorMy_NameorMy_name.
Formatting
Indentation is 4 spaces.
//is used for single-line comments,/* ... */for multi-line comments.If a function’s parameters or procedure’s parameters are too long to fit on a single line, the parameters all go on one or more separate lines and are double-indented (8 spaces).
Statements and specifications that are too long for a single line are broken into multiple lines, with the extra lines indented 4 spaces more than the first line.
Binary operators have spaces around them:
x * y,x / y,x % y,x + y, …,x <==> y. Colons do not:x:int. Commas have spaces after them:(x, y, z)..if,while,forall, andlet existsstatements have a space before parentheses:if (...),while (...),forall (...),let exists (...). In other places, there is no space before parentheses:my_lemma(...),my_function(...).Curly brackets
{and}, for multi-line blocks of statements, go on their own line. This is largely becauseprocedureandwhileloops have specifications (requires,invariant, etc.) that get in the way of a{appearing on the same line as theprocedureorwhilekeyword.Each procedure attribute gets its own line.
Specification keywords like
requires,ensures,modifies, etc. are single-indented relative to a procedure orwhileloop. The specification expressions appear on a separate line from the specification keywords and are indented 4 spaces more than the keywords.
Example:
// This is a short procedure
procedure ShortProc(ghost x:int, ghost y:int)
modifies
eax;
{
Add(eax, 1);
}
/*
This is a longer procedure.
Its parameters don't fit on a line, so they are indented 8 spaces.
*/
procedure MyLongProcedure(
inline b:bool,
inout dst:reg, in src:reg,
ghost apple_banana:bool, ghost cat_dog:int, ghost earth_fire:int)
{:public}
{:timeLimit 10}
modifies
eax; ebx;
requires
10 <= eax < 20;
ebx == (if apple_banana then cat_dog else
7 * (earth_fire + src));
{
inline if (b)
{
while (eax < 100)
invariant
0 <= eax <= 100;
decreases
100 - eax;
{
Add(eax, 1);
MyOtherLongProcedure(b, dst, src, apple_banana, cat_dog,
7 * (earth_fire + src), eax, ebx);
my_lemma(cat_dog);
}
}
}