Types, functions, and expressions

As mentioned in Programs and procedures, a Vale program contains a series of top-level declarations. These top-level declarations may be:

  • type declarations and operand type declarations

  • global variable declarations

  • const and function declarations

  • procedure declarations

  • verbatim blocks (see Verbatim blocks)

Vale processes declarations in the order they appear in the program. The order matters, because each declaration can refer to earlier declarations but not later declarations. All declared names (types, variables, constants, functions, procedures) live in a single namespace: you cannot have a type, a function, and a procedure with the same name. For any name x, there may be up one non-extern top-level declaration named x or multiple extern declarations named x. If two top-level extern declarations with the same name are declared, the later declaration hides the earlier one.

For compatibility with Dafny modules and FStar modules, names may contain . symbols, as in FStar.Pervasives.option.

Global variables, constants, functions, and procedures have types. Vale has a simple type system with polymorphism but without dependent types. Because Vale’s type system is simpler than that of some verification frameworks, such as FStar’s, there may be expressions from the verification framework that Vale’s type system cannot type-check. As described in the next section, a Vale program can use type casts to access such expressions. For formal details on Vale’s type system, see here.

Types

Vale has a small number of built-in types and can import other types from the underlying verification framework. The type x ... extern declaration imports types from the verification framework:

type char:Type(0) extern;
type option(a:Type(0)):Type(0) extern;
type map(a:Type(0), b:Type(0)):Type(0) extern;

Types can have type parameters like a:Type(0). For example, the map type shown above takes parameters a and b, which can be instantiated with types:

let x:map(int, option(bool)) := ...;

Every type declaration specifies a kind for each type parameter and a return kind. The most common kind is Type(0), and for Dafny, Type(0) is the only kind that is needed. However, FStar is more complicated does not allow all types to have the same kind. FStar’s prop type, for example, has kind Type(1). Therefore, Vale also supports kinds Type(1), Type(2), and so on.

Vale provides the following built-in primitive types:

  • bool, containing constants true and false and used for operators like &&, ||, and ==>.

  • prop (FStar only), which FStar uses instead of bool for forall and exists. Vale uses the same constants true and false and &&, ||, and ==> for prop as for bool, and will automatically generate the appropriate FStar operators as necessary (e.g. generating FStar’s /\ or && from Vale’s && as appropriate). In Vale, bool is a subtype of prop, so values of type bool can be used where a value of type prop is expected.

  • int, containing all mathematical integers …, (-2), (-1), 0, 1, 2, …

  • int_range(I1, I2), containing integers in the range I1…I2 (including I1 and I2). I1 and I2 must be integer constants or the symbol _, representing no bound (i.e. negative or positive infinity). For example, if x has type int_type(0, _), then x + 1 will have type int_type(1, _). Smaller range types are subtypes of larger range types and of int, so that a value of type int_type(1, _) can be used where a value of type int_type(0, _) or int is expected.

  • tuple(t1, ..., tn) is the type of tuples containing components of type t1 … tn, created by expressions tuple(e1, ..., en).

  • fun(t1, ..., tn) -> t0 is type of functions accepting arguments of type t1 … tn and returning type t0.

In addition, Vale is aware of the following types, although they must be declared explicitly as type x ... extern; declarations with a {:primitive} attribute (see Attributes):

  • state, the type of the program’s state (the built-in expression this has type state)

  • string, the type of string literals

  • list(t) (FStar only), the type of list literals list(e1, ..., en)

  • seq(t) (Dafny only), the type of sequence literals seq(e1, ..., en)

  • set(t) (Dafny only), the type of set literals set(e1, ..., en)

The type x ... := ...; syntax declares type abbreviations:

type my_bool:Type(0) := bool;
type nat:Type(0) := int_range(0, _);
type pos:Type(0) := int_range(1, _);
type byte:Type(0) := int_range(0, 0xff);
type int_map(a:Type(0)):Type(0) := map(int, a);

Within Vale’s type system, type abbreviations like nat are equivalent to the types that they abbreviate, like int_range(0, _). When generating Dafny/FStar code, Vale attempts to preserve abbreviations, so that if variable x has type nat in the Vale code, it will have type nat in the Dafny or FStar code, not int_range(0, _). Vale will not generate a declaration of the nat type itself, so nat must be declared manually in separate Dafny or FStar code. Also note that raw int_range types do not have built-in equivalents in Dafny and FStar: int_range is translated into int in Dafny and into refinements of int in FStar.

extern procedures and functions can be polymorphic over types:

ghost procedure g1#[a:Type(0), b:Type(0)](ghost x:a, ghost y:b)
    extern;

ghost procedure g2()
{
    g1(10, true);
    g1#[int, bool](10, true);
}

The explicit type arguments #[int, bool] are optional; without them, Vale will try to infer type arguments.

The syntax #t(e) or #(t)(e) casts expression e to type t:

ghost procedure cast_test(ghost i:int)
    requires
        i >= 0;
{
    let n:nat := #nat(i);
}

The cast in this example is needed because i’s type int is not a subtype of n’s type nat.

Although Vale does not have dependent types, it has some limited support for interacting with some of FStar’s dependent types:

type buf_typ:Type(0) extern;
const bt32:buf_typ extern;
const bt64:buf_typ extern;
type buf(bt:Dependent(buf_typ)):Type(0) extern;
type buf32:Type(0) := buf(dependent(bt32));
type buf64:Type(0) := buf(dependent(bt64));
function buf_len #[bt:Dependent(buf_typ)](b:buf(bt)):int extern;

If an expression xe has type xt, then the type dependent(xe) has kind Dependent(xt). In the example above, this allows type buf to take a value bt as a type parameter and allows buf_len to be polymorphic over values bt of type buf_typ, as in a dependent type system. (From Vale’s perspective, bt is promoted to a type in order to use ordinary polymorphism over types.) However, xe must be a global constant and xt must be simple named type, so this is only useful in limited situations.

Operands and operand types

Vale expressions have types, while procedure operands have operand types. Operand types describe both the type of the value carried by the operand (e.g. an integer) and the location of the operand. Locations may be global variables (typically registers), constants, or dynamically constructed locations (typically memory addresses). Here is an example of operand type declarations for x64 assembly language:

type nat64:Type(0) := int_range(0, 0xffff_ffff_ffff_ffff);

operand_type reg64:nat64 :=
| inout rax | inout rbx | inout rcx | inout rdx
| inout rsi | inout rdi | inout rbp | inout r8
| inout r9 | inout r10 | inout r11 | inout r12
| inout r13 | inout r14 | inout r15
;

operand_type shift_amt64:nat64 := in rcx | const;
operand_type Mem64(in base:reg64, inline offset:int):nat64;
operand_type dst_opr64:nat64 := reg64 | Mem64;
operand_type opr64:nat64 := dst_opr64 | const;

This declares a series of operand types:

  • operand type reg64, for 64-bit values (of type nat64) located in registers rax … r15, usable as both input and output operands.

  • operand type shift_amt64, for x64 shift instructions that require the shift amount in either register rcx or as a constant.

  • operand type Mem64, for 64-bit values located in memory.

  • operand type dst_opr64, for operands that can be either a register or memory operand

  • operand type opr64, for operands that can be either a register, memory operand, or constant. (Note that const is a built-in Vale keyword, not an operand type.)

For example, an x64 shift-left instruction can be declared to take a destination operand of operand type dst_opr64 and a source operand of type shift_amt64:

procedure Shl64(inout dst:dst_opr64, in amt:shift_amt64)

Operand constructors and memory

Locations can be constructed dynamically with operand constructors like Mem64. Such constructors can take other operands as arguments:

Shl64(Mem64(rax, 60), 16);

Each operand constructor requires operand procedures for reading and/or writing the location specified by the operand constructor. The operand procedures have the name of the operand constructor concatenated with the suffix “_in” or “_out”:

var mem:map(int, byte) {:state mem()};

procedure Mem64_in(in base:reg_opr64, inline offset:int) returns(o:operand)
    {:operand}
    reads
        mem;
    extern;

procedure Mem64_out(in base:reg_opr64, inline offset:int, in o:operand)
    {:operand}
    modifies
        mem;
    extern;

In the first procedure, the operand o contains the value loaded from memory. In the second procedure, the operand o contains the value being stored to memory. Operand procedures can optionally have requires and ensures to specify properties of o and of the other parameters to the procedures. Operand procedures can also read and write global variables like mem.

Operand values and locations

Vale procedures can refer to both the value and location of an operand. For an operand parameter x, the expression x contains the operand’s value, while the expression @x contains the operand’s location. This can be used, for example, to require two operands to be in distinct registers:

procedure IncrTwo(inout dst1:reg64, inout dst2:reg64)
    requires
        dst1 < 100;
        dst2 < 100;
        @dst1 != @dst2;
    ensures
        dst1 == old(dst1) + 1;
        dst2 == old(dst2) + 1;
{
    Add(dst1, 1);
    Add(dst2, 1);
}

To use @x, x’s operand type must declare a type for locations, using the @ t syntax. The following declaration, for example, tells Vale that the expressions @dst1 and @dst2 should have type operandImpl:

operand_type reg64:nat64 @ operandImpl :=
| inout rax | inout rbx | inout rcx | inout rdx
...

Functions and consts

Vale can import functions and constants from the verification framework using const x ... extern and function x ... extern declarations:

const seven:int extern;

function sum3(x:int, y:int, z:int):int extern;

function sqr(x:int):(z:int)
    ensures
        z >= 0;
    extern;

function id#[a:Type(0)](x:a):a extern;

ghost procedure test_functions()
{
    assert seven == 7;

    assert sum3(10, 20, 30) == 60;
    assert sqr(10) == 100;
    assert id(10) == 10;
    assert id#[int](10) == 10;

    let f:fun(int, int, int) -> int := sum3;
    assert f(10, 20, 30) == 60;

    let g:fun(int) -> int := id;
    assert g(10) == 10;
}

Polymorphic functions like id can be applied to type arguments using #[...]; otherwise, Vale will try to infer the type arguments. Monomorphic functions have function types fun(...) -> ...; polymorphic functions can be coerced to monomorphic function types, as with g in the example above.

Dafny and FStar can declare opaque functions whose definitions are hidden from the verifier unless explicitly revealed. Vale can reveal an opaque function’s definition with reveal f:

function opaque_sum(x:int, y:int):int extern;

ghost procedure test_opaque()
{
    reveal opaque_sum;
    assert opaque_sum(10, 20) == 30;
}

Custom operators

Vale programs can abbreviate one-argument and two-argument functions as custom unary and binary operators. Such operators are not overloaded — there can only be one function for each operator name — but Vale programs can create as many operator names as desired.

The Lexical structure section describes how to use the #token directive to create new operator names (operator tokens). After creating a name, the Vale code declares a function abbreviation using the function operator(...) ... := ... syntax:

#token #+# precedence +
#token +. precedence +
#token *. precedence *
#token %. precedence *
#token ~~ precedence !
function operator(#+#) (a:int, b:int):int := opaque_sum;
function operator(+.) (a:poly, b:poly):poly := poly_add;
function operator(*.) (a:poly, b:poly):poly := poly_mul;
function operator(%.) (a:poly, b:poly):poly := poly_mod;
function operator(~~) (a:quad32):poly := quad32_to_poly;

ghost procedure test_opaque()
{
    reveal opaque_sum;
    assert 10 #+# 20 == 30;
}

Overloaded operators

Vale supports a small set of overloadable operators:

  • .fieldname for reading a field of a datatype

  • .fieldname := for updating a field of a datatype with some value

  • [] for reading an item in a collection based on some key

  • [ := ] for updating an item in a collection based on some key and value

  • ?[] for testing whether a collection contains a key

Each of these operators can have many implementations. Each implementation is declared to Vale with a function operator(...) ... extern declaration:

type int_pair:Type(0) extern;
function Mkint_pair(fst:int, snd:int):int_pair extern;

function operator(.fst) (p:int_pair):int extern;
function operator(.snd) (p:int_pair):int extern;
function operator(.fst :=) (p:int_pair, v:int):int_pair extern;
function operator(.snd :=) (p:int_pair, v:int):int_pair extern;

type seq(a:Type(0)):Type(0) extern;
type map(a:Type(0), b:Type(0)):Type(0) extern;

function length#[a:Type(0)](s:seq(a)):nat extern;

function operator([])     #[a:Type(0)](s:seq(a), i:int):a extern;
function operator([ := ]) #[a:Type(0)](s:seq(a), i:int, v:a):seq(a) extern;
function operator([])     #[a:Type(0), b:Type(0)](m:map(a, b), key:a):b extern;
function operator([ := ]) #[a:Type(0), b:Type(0)](m:map(a, b), key:a, v:b):map(a, b) extern;
function operator(?[])    #[a:Type(0), b:Type(0)](m:map(a, b), key:a):bool extern;

ghost procedure test_overload(ghost s:seq(nat), ghost m:map(int, nat))
    requires
        length(s) > 3;
{
    let x := Mkint_pair(10, 20);
    assert x.fst == 10;
    assert x.snd == 20;
    let x2 := x.(fst := 11);
    assert x2.fst == 11;
    assert x2.snd == 20;

    let s2:seq(nat) := s[3 := 30];
    assert s2[3] == 30;

    assert m?[100] ==> m[100] >= 0;
}

When an expression like m[100] uses an overloaded operator like operator([]), Vale must decide which of the various operator([]) implementations is appropriate. To do this, it computes the type t of m, simplifies t until it is an extern type rather than a type abbreviation, and then uses t’s name (map in this case) for disambiguation. Thus, there can be one operator([]) for map and one for seq, but not more than one for map or more than one for seq.

Expressions

See the Complete Vale syntax section for a complete list of Vale expressions. The following expressions are described in other sections:

Arithmetic operators *, /, %, +, and - compute new int and int_range values from existing int and int_range values (see Types or the formal type rules). Integer comparison operators <, >, <=, and >= compute bool values from int and int_range values.

Comparisons can be chained together: a <= b < c <= d is an abbreviation for a <= b && b < c && c <= d.

Equality == and inequality != compute bool values (in Dafny) or prop values (in FStar).

e is C tests whether a datatype value e is an instance of datatype constructor C (like Dafny’s e.C? or FStar’s C? e).

Logical operators !, &&, ||, ==>, <==, and <==> compute bool values from existing bool values in Dafny. For FStar, they work on both bool and prop values.

if e1 then e2 else e3 selects either e2 or e3 based on e1 of type bool.

let x := e1 in e2 introduces a variable x, equal to e1, in e2.

fun(x1:t1, ..., xn:tn) e, sometimes known as a “lambda”, creates an anonymous function with parameters x1 … xn and body e.

this computes the current state (i.e. all register values, memory values, etc.), of type state. The state type is not defined by Vale, but is instead user-defined in the underlying verification framework (see va_state in Interface with verification framework). Most procedures shouldn’t refer to this, but it is occasionally used for implementing instructions (see Instructions), which can read this or assign this := ....

Quantifiers

Vale supports two quantifiers, forall and exists. The expression forall(x1:t1, ..., xn:tn) e means that e is true for all values that can be assigned to variables x1 … xn of type t1 … tn. The expression exists(x1:t1, ..., xn:tn) e means that e is true for at least one assignment of values to variables x1 … xn of type t1 … tn. In Dafny, forall and exists expressions have type bool. In FStar, they have type prop.

forall and exists, used in combination with other expressions like arithmetic and function application, are often difficult for verification frameworks to reason about completely automatically. Specifically, it’s hard for the verification framework to answer these two questions:

  • If the verifier knows forall(x1:t1, ..., xn:tn) e and wants to use this to prove some formula Q, which values should it instantiate x1 … xn with? For example, if it knows forall(x:int) p(x + x) == x + x + x, which x should it choose to prove p(10) == 15? (In this example, x = 5 is a good choice, but it’s not obvious how a verifier should guess this automatically.)

  • If the verifier wants to prove exists(x1:t1, ..., xn:tn) e, which values for x1 … xn should it choose to prove e? For example, it can prove exists(x:int) 2 * x == x + 10 with x = 10, but it’s not obvious how to guess this automatically, especially in more complicated examples.

Dafny and FStar rely on triggers (also called patterns) to determine how to use forall expressions and how to prove exists expressions. For example, suppose the verifier knows forall(x:int, y:int) f(x, y) == x + y and wants to prove f(2, 3) == 5. This can be proven with x = 2, y = 3, which the verifier can guess by matching the expression f(x, y) with the expression f(2, 3). To enable this matching, a Vale program annotates the forall expression with the trigger {f(x, y)}, which tells the verifier to try to find terms of the form f(..., ...) and match them to f(x, y):

forall(x:int, y:int){f(x, y)} f(x, y) == x + y

A trigger can have more than one expression in it; the trigger fires if all the expressions in the trigger are matched:

forall(x:int, y:int){f(x), g(y))} f(x) == g(y)

There can also be more than one trigger; the verifier tries to match any of them.

Dafny will automatically infer the triggers shown in the examples above, so the Vale code can safely omit them. However, FStar will not infer them, so it’s a good idea to always write the triggers explicitly when using FStar. (Without the triggers, FStar lets the underlying SMT solver choose the triggers, and these triggers tend to be dangerously aggressive, leading to slow proofs and timeouts.)

Even when using Dafny, not all quantified expressions have good triggers. The expression forall(x:int) p(x + x) == x + x + x, for example, cannot be matched with p(10) == 15 to produce x = 5 in any obvious way, since p(10) == 15 doesn’t contain 5 anywhere. Dafny’s automatic inference of triggers doesn’t help, since there is no good trigger to infer. Therefore, it’s wise to use quantified expressions that have good triggers. For example, the expression forall(y:int) y % 2 == 0 ==> p(y) == y / 2 * 3 can use {p(y)} as a trigger (and Dafny will infer this trigger automatically). This is logically equivalent to the earlier expression, but enables better automation.

There are two other questions relevant to quantifiers (the flip side of the two earlier questions):

  • How does a verifier prove forall(x1:t1, ..., xn:tn) e?

  • How does a verifier use exists(x1:t1, ..., xn:tn) e to prove some formula Q?

Compared with the two earlier questions, these are relatively easy and do not require triggers. For example, a verification framework can prove forall(x1:t1, ..., xn:tn) e simply by trying to prove e with variables x1 … xn in scope. There is no need to instantiate x1 … xn with particular values to do this, so there is no decision to make on which values to instantiate x1 … xn with. However, e itself could be difficult to prove, and the verification framework may need hints to complete the proof of e, such as calls to lemmas. Vale programs can use a forall statement to supply such hints:

function f1(x:int, y:int):bool extern;
function f2(x:int, y:int):bool extern;

ghost procedure lemma_f1_f2(ghost x:int, ghost y:int)
    requires
        f1(x, y);
    ensures
        f2(x, y);
    extern;

ghost procedure test_forall()
    ensures
        forall(x:int, y:int){f1(x, y)}{f2(x, y)} f1(x, y) ==> f2(x, y);
{
    forall (x:int, y:int){f2(x, y)}
        f1(x, y) implies f2(x, y) by
    {
        lemma_f1_f2(x, y);
    }
}

In this example, the forall (x:int, y:int)...{...} statement proves forall(x:int, y:int){f2(x, y)} f1(x, y) ==> f2(x, y), which in turn proves test_forall’s postcondition.

For exists, a let exists statement (Dafny-only, not FStar) can extract variables from an exists expression in order to use those variables to prove other expressions, such as the precondition to lemma_f1_f2 in the following example:

ghost procedure test_exists()
    requires
        exists(x:int, y:int){f1(x, y)} f1(x, y);
{
    // Ask verifier to choose some x and y such that f1(x, y):
    let exists (x:int, y:int){f1(x, y)} f1(x, y);
    // Now we have x and y as local ghost variables and we can use them:
    lemma_f1_f2(x, y);
}