.. highlight:: vale


.. _interface:

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:

#. Run the Vale tool to compile the Vale code to Dafny/FStar code.
#. Verify the generated Dafny/FStar code.
#. 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 :ref:`verbatim` 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:

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