Interface with verification framework

Vale generates functions and lemmas to represent procedures defined in Vale source code. It also generates temporary variable names inside generated code. To avoid conflicts between native names in the verification language and Vale-generated names, a convention is used for each verification language for Vale-generated names:

  • All Vale-generated Dafny and FStar names begin with the prefix va_. Hand-written Dafny and FStar code should avoid names beginning with va_ if the hand-written code will be linked with the Vale-generated code.

Vale source code may freely reference definitions in the verification language. For example, Vale/Dafny code may refer to types such as real and bool, as well as user-defined types, functions, and methods. These names are unmangled when translating from the Vale source language to the verification language: the names bool and real in Vale source code are translated into the names bool and real in the verification language, not va_bool and va_real.

Vale-generated code

Generating executable assembly language from Vale code takes three steps:

  1. Run the Vale tool to compile the Vale code to Dafny/FStar code.

  2. Verify the generated Dafny/FStar code.

  3. Run the generated Dafny/FStar code to print the assembly language code.

For each procedure P in the generated code, the Vale tool generates two objects in the verification language:

  • a function va_code_P that builds the executable code for the procedure

  • a lemma va_lemma_P that proves that the executable code for the procedure satisfies its postconditions, assuming its preconditions

As an example, suppose that a Vale procedure P consists of two calls to a procedure named Increment, passing a register named eax as an argument:

var ok:bool {:state ok()};
var eax:int {:state reg(EAX)};
var ebx:int {:state reg(EBX)};

procedure Increment(inout x:reg)
    ensures
        x == old(x) + 1;
    extern;

procedure P()
    modifies
        eax;
    requires
        eax >= 0;
    ensures
        eax >= 2;
{
    Increment(eax);
    Increment(eax);
}

For procedure P, the Vale tool generates a Dafny function va_code_P that builds a value of type code. (Generated FStar code is similar, though with FStar syntax.) This value contains two values constructed by va_code_Increment:

function method{:opaque} va_code_P():va_code
{
  va_Block(
    va_CCons(va_code_Increment(va_op_reg_reg(EAX)),
    va_CCons(va_code_Increment(va_op_reg_reg(EAX)),
    va_CNil())))
}

The Vale tool also generates a lemma that proves the correctness of the code for P:

lemma va_lemma_P(va_b0:va_codes, va_s0:va_state, va_sN:va_state)
  returns (va_bM:va_codes, va_sM:va_state)
  requires va_require(va_b0, va_code_P(), va_s0, va_sN)
  ensures  va_ensure(va_b0, va_bM, va_s0, va_sM, va_sN)
  requires va_get_ok(va_s0)
  ensures  va_get_ok(va_sM)
  requires va_get_reg(EAX, va_s0) >= (0)
  ensures  va_get_reg(EAX, va_sM) >= (2)
  ensures  va_state_eq(va_sM, va_update_reg(EAX, va_sM, va_update_ok(va_sM, va_s0)))
{
  reveal_va_code_P();
  var va_old_s:va_state := va_s0;
  ghost var va_ltmp1, va_cM:va_code, va_ltmp2 := va_lemma_block(va_b0, va_s0, va_sN);
  va_sM := va_ltmp1;
  va_bM := va_ltmp2;
  var va_b1:va_codes := va_get_block(va_cM);
  ghost var va_b2, va_s2 := va_lemma_Increment(va_b1, va_s0, va_sM, va_op_reg_reg(EAX));
  ghost var va_b3, va_s3 := va_lemma_Increment(va_b2, va_s2, va_sM, va_op_reg_reg(EAX));
  va_sM := va_lemma_empty(va_s3, va_sM);
}

The lemma ensures that if P’s preconditions are satisfied (eax >= 0) then the code never crashes, and the code either runs forever or terminates in a state satisfying P’s postconditions (eax >= 2).

More specifically, the lemma describes the effect of the code running on some initial state va_s0 of type va_state. The postcondition ensures va_get_ok(...) ensures that if the preconditions to P are satisfied, then the evaluation will never crash. The postcondition va_get_reg(EAX, va_sM) >= 2 ensures that in the final state va_sM, the variable eax will be at least 2. To prove its postconditions va_lemma_P relies on the postconditions of va_lemma_Increment. Each of P’s calls to Increment generates one call to the lemma va_lemma_Increment.

After verification, the generated Dafny code may be compiled and linked in with a trusted Dafny Main method. This Main method can, for example, print the code value generated by va_code_P() as assembly language instructions. (See Verbatim blocks for an example.) These instructions may then be assembled and executed. The details of the generated code may vary depending on the exact version of the tool. (To see examples of up-to-do date generated code, try running the Vale tool and examining the generated code.)

Instructions

For the example procedure P from the previous section, Vale generates functions va_code_P and va_lemma_P automatically. The increment procedure Increment, however, is declared extern, and Vale does not generate code for extern declarations. It’s possible to write the Dafny (or FStar) va_code_Increment and va_lemma_Increment functions manually, but this is inconvenient.

The {:instruction ...} attribute provides a more convenient approach than extern to implement Increment and other primitive instructions:

procedure Increment(inout x:reg)
    {:instruction Ins(InsAdd(x, OConst(1)))}
    ensures
        x == old(x) + 1;
{
    // empty body in this example,
    // but can contain additional ghost code if needed
}

Vale generates a va_code_Increment function containing the expression from the {:instruction ...} attribute:

function method{:opaque} va_code_Increment(x:va_operand_reg):va_code
{
  Ins(InsAdd(x, OConst(1)))
}

lemma va_lemma_Increment(va_b0:va_codes, va_s0:va_state, va_sN:va_state, x:va_operand_reg)
  returns (va_bM:va_codes, va_sM:va_state)
  requires va_require(va_b0, va_code_Increment(x), va_s0, va_sN)
  requires va_is_dst_reg(x, va_s0)
  ensures  va_ensure(va_b0, va_bM, va_s0, va_sM, va_sN)
  requires va_get_ok(va_s0)
  ensures  va_get_ok(va_sM)
  ensures  va_eval_reg(va_sM, x) == va_eval_reg(va_s0, x) + 1
  ensures  va_state_eq(va_sM, va_update_ok(va_sM, va_update_operand_reg(x, va_sM, va_s0)))
{
  reveal_va_code_Increment();
  var va_old_s:va_state := va_s0;
  va_ins_lemma(Ins(InsAdd(x, OConst(1))), va_s0);
  ghost var va_ltmp1, va_cM:va_code, va_ltmp2 := va_lemma_block(va_b0, va_s0, va_sN);
  va_sM := va_ltmp1;
  va_bM := va_ltmp2;
}

Vale also generates a va_lemma_Increment that reveals the definition of va_code_Increment and calls a user-supplied lemma va_ins_lemma, as shown above. If these are insufficient to prove va_lemma_Increment’s postconditions, the body of the Vale P procedure can also contain additional ghost code, such as calls to lemmas, as hints to complete the proof.

For the definitions above to succeed, the programmer must manually supply definitions of instructions and their semantics:

// Manually-written Dafny code:
datatype register = EAX | EBX
datatype operand = OReg(r:register) | OConst(n:int)
datatype ins =
  InsAdd(dstAdd:register, srcAdd:operand)
| InsSub(dstAdd:register, srcAdd:operand)
datatype code =
  Ins(ins:ins)
| Block(block:codes)
| IfElse(ifCond:ocmp, ifTrue:code, ifFalse:code)
| While(whileCond:ocmp, whileBody:code)
datatype codes = CNil() | CCons(hd:code, tl:codes)
...
predicate eval_ins(ins:ins, s0:state, sN:state)
{
    ...
        match ins
            case InsAdd(dst, src) =>
                sN == update_reg(dst, s0, eval_reg(dst, s0) + eval_opr(src, s0))
            ...
}
type va_operand_reg = register
...

Vale libraries

When Vale generates code in the chosen verification language (Dafny or FStar), the generated code refers to types, functions, and lemmas that are assumed to be provided by some user-defined library. The following tables list these types, functions, and lemmas.

The following types, functions, and lemmas are assumed to be provided by a library. Each name in the table is mangled according to the convention described above. For example, state will be written referred to as va_state by Vale-generated Dafny code. Types written as ... are unconstrained by Vale and may be chosen by the library. The symbols t and O refer to types and operand types. The symbol f refers to fields of the state type. A special operand type O = cmp is used for conditionals in if/else and while/for statements.

  • Types:

    • state

    • code

    • codes – list of code

    • value_O – type of O values, e.g. va_value_reg = int

    • operand_O – type of O operands, e.g. va_operand_reg = register

  • Lemmas:

    • lemma_ifElse

    • lemma_while

    • lemma_whileTrue

    • lemma_whileFalse

    • lemma_whileInv

    • lemma_empty

    • lemma_block

    • ins_lemma – used in {:instruction} procedures

  • General functions:

    • CNil():codes

    • CCons(hd:code, tl:codes)

    • require(b0:codes, c1:code, s0:state, sN:state):bool

    • ensure(b0:codes, b1:codes, s0:state, s1:state, sN:state):bool

    • state_eq(s0:state, s1:state):bool

    • cmp_x(o1:cmp, o2:cmp):cmp for each comparison function x, where x is either a user-defined function name (for conditional expressions x(o1, …, on)) or one of eq, ne, le, ge, lt, or gt (for conditional expressions o1 == o2, o1 != o2, etc.)

    • get_block(c:code):codes

    • get_ifCond(c:code):cmp

    • get_ifTrue(c:code):code

    • get_ifFalse(c:code):code

    • get_whileCond(c:code):cmp

    • get_whileBody(c:code):code

    • whileInv(b:cmp, c:code, n:int, r1:state, ok1:bool, r2:state, ok2:bool):bool

    • IfElse(cond:cmp, ift:code, iff:code):code

    • While(cond:cmp, body:code):code

    • Block(block:codes):code

  • Functions for operand types O:

    • eval_O(s:state, o:O):t – evaluate operand o in state s

    • is_src_O(o:O):bool – o is a valid source operand

    • is_dst_O(o:O):bool – o is a valid destination operand

    • update_operand_O(o:O, sM:state, sK:state):state – return sK updated with a copy of operand o evaluated in sM

    • const_O(v:t):O – coerce constant value v to a constant operand

    • coerce_O1_to_O2 – coerce O1 to O2

  • Functions for state fields f:

    • op_O_f(…):O – build operand O from f or f(…)

    • get_f(…, s:state):t – get field f or f(…) from state s

    • update_f(…, sM:state, sK:state):state – return sK updated with a copy of sM’s field f or f(…)

  • Functions and procedures for operand constructors P(…params…):

    • opr_code_P(…non-ghost params…):operand_type – construct operand for P

    • opr_lemma_P(state, …params…):operand_type (Dafny only) – lemma called for each occurrence of P

    • P_lemma(…params as ghost…) (FStar only) – Vale procedure (no va_ prefix) called for each occurrence of P

  • Functions for overloaded collection operators with name x (currently FStar only):

    • va_subscript_x(c:container, k:key):value

    • va_update_x(c:container, k:key, v:value):container

    • va_contains_x(c:container, k:key):bool