doc/index.html

<html>
<body>
  <i>Warning: this document is likely to be revised repeatedly as Vale evolves.  It may lead or lag the actual Vale implementation.</i>

  <h1>An Overview of Vale (Verified Assembly Language for Everest)</h1>

  <p>
    Vale is a tool and syntax for developing verified low-level code:

    <ul>
      <li>
        <b>Tool and syntax.</b>
        Vale code is written in a C-style syntax.
        The Vale tool translates Vale code into a form that may be verified and executed.
      </li>
      <li>
        <b>Verified code.</b>
        Vale supports Hoare-logic style reasoning with preconditions, postconditions, and loop invariants.
      </li>
      <li>
        <b>Low-level code.</b>
        Vale is designed for verifying code at the level of assembly language or register-transfer languages.
        It is not designed to support higher-level features such as complex expression evaluation, object orientation, or higher-order functions.
        It does, however, support basic control constructs such as if/else statements, while loops, and procedure calls.
      </li>
    </ul>

  <p>
    Although Vale supplies a syntax for writing programs, Vale is not a complete, standalone language.
    Instead, Vale is designed to be used on top of an existing verification language, such as Dafny, FStar, or Lean.
    (Currently, only Dafny is supported.)
    The existing verification language supplies semantics to programs.
    Programs written for Vale/Dafny, for example, use Dafny type checking rules and verification rules,
    while programs written for Vale/FStar use FStar type checking rules and verification rules.
    Thus, Vale/Dafny, Vale/FStar, and Vale/Lean are complete and independent languages;
    programs written and verified in Vale/Dafny, for example, may not be valid Vale/FStar programs.

  <h2>Contents</h2>

    <a href="#verification">Verification, compilation, and execution</a><br />
    <a href="#running">Running the Vale tool</a><br />
    <a href="#syntax">Vale syntax</a><br />
    <a href="#procedures">Procedures</a><br />
    <a href="#overloading">Operator overloading</a><br />
    <a href="#interface">Interface between Vale and verification languages</a><br />

  <h2 id="verification">Verification, compilation, and execution</h2>

  <p>
    Generating executable assembly language from Vale code takes two steps:
    first, compile the Vale code to Dafny/FStar/Lean code,
    and second, verify and execute the Dafny/FStar/Lean code to generate assembly language code.
    In the first step, the Vale tool translates Vale code into the corresponding verification language:
    Vale/Dafny code becomes Dafny code, Vale/FStar becomes FStar code, and so on.
    In the second step, the corresponding tool (Dafny, FStar, etc.) is invoked to verify, compile, and execute the generated code;
    executing the generated code produces assembly language.

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

    <ul>
      <li>a function that builds the executable code for the procedure</li>
      <li>a lemma that proves that the executable code for the procedure satisfies its postconditions, assuming its preconditions</li>
    </ul>

  <p>
    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:

    <pre><code>
      procedure Increment(inout register x:int)
        ensures
          x == old(x) + 1;
      { ... }

      var{:state reg(EAX)} eax:int;

      procedure p()
        modifies
          eax;
        requires
          eax &gt;= 0;
        ensures
          eax &gt;= 2;
      {
        Increment(eax);
        Increment(eax);
      }
    </code></pre>

  <p>
    For procedure p, the Vale/Dafny tool generates a Dafny function va_code_p that builds a value of type code.
    This value contains two values constructed by va_code_Increment:

    <pre><code>
      function method{:opaque} va_code_p():va_code
      {
        ...
        va_CCons(va_code_Increment(va_op_register_reg(EAX)),
        va_CCons(va_code_Increment(va_op_register_reg(EAX)),
        va_CNil()))
        ...
      }
    </code></pre>

  <p>
    The Vale/Dafny tool also generates a lemma that proves the (partial) correctness of the code for p:

    <pre><code>
      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_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
        ...
      {
        ...
        ghost var va_b2, va_s2 := va_lemma_Increment(va_b1, va_s0, va_sM, va_op_register_reg(EAX));
        ghost var va_b3, va_s3 := va_lemma_Increment(va_b2, va_s2, va_sM, va_op_register_reg(EAX));
        ...
      }
    </code></pre>

  <p>
    The lemma ensures that if p's preconditions are satisfied (eax &gt;= 0)
    then the code never fails,
    and the code either runs forever or terminates in a state satisfying p's postconditions (eax &gt;= 2).

  <p>
    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 be a failure.
    The postcondition va_get_reg(EAX, va_sM) &gt;=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.

  <p>
    For more details about code values and lemmas, see the
    <a href="#interface">Vale interface</a> section.

  <p>
    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 <a href="#verbatim">here</a> 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, as described in the next section.

  <h2 id="running">Running the Vale tool</h2>

  <p>
    The following options may be supplied to vale.exe:

    <table border="1">
      <tr><td>-in &lt;filename.vad&gt;</td><td>specify one or more input .vad files</td></tr>
      <tr><td>-out &lt;filename.dfy&gt;</td><td>specify the output .dfy file</td></tr>
    </table>

  <h2 id="syntax">Vale syntax</h2>

  <p>
    Notation:
    <ul>
      <li><i>[</i>A<i>]</i> indicates that A is optional.</li>
      <li>A...A indicates that A is repeated zero or more times.</li>
      <li>A<i>[</i>...A<i>]</i> indicates that A is repeated one or more times.</li>
      <li>Variable/attribute/function/procedure/constructor/field/type names are written as "x", "f", "p", "c", "fd", "t",
          where "f" is used to emphasize a function name,
          "p" is used to emphasize a procedure name,
          "c" is used to emphasize a datatype constructor name,
          "fd" is used to emphasize a field name,
          and "t" is used to emphasize a type name.</li>
    </ul>

  <p>
    For conciseness, the following table omits attributes.
    Attributes are listed in a <a href="#attributes">separate section</a>.

  <p>
    <table border="1">
    <tr><td>Grammar</td><td>Examples and notes</td></tr>
    <tr>
    <td>
    <pre>

PROGRAM ::= INCLUDE ... INCLUDE DECL ... DECL

INCLUDE ::= include "STRING"

DECL ::=
  | <a href="#state">var</a> x : TYPE ;
  | function f ( FORMALS ) : TYPE <i>[</i>:= f<i>]</i> ;
  | <a href="#procedures">procedure</a> p ( PFORMALS ) <i>[</i>returns ( PRETS )<i>]</i> SPECS { STMTS }
  | <a href="#procedures">procedure</a> p ( PFORMALS ) <i>[</i>returns ( PRETS )<i>]</i> SPECS extern ;
  | <a href="#procedures">procedure</a> p ( PFORMALS ) <i>[</i>returns ( PRETS )<i>]</i> <a href="#overloading">:= p ;</a>
  | <a href="#verbatim">VERBATIM_DECL_BLOCK</a>

FORMALS ::= FORMAL , ... , FORMAL
FORMAL ::= x <i>[</i>: TYPE<i>]</i>

PFORMALS ::= PFORMAL , ... , PFORMAL
<a href="#parameters">PFORMAL</a> ::=
  | ghost x : TYPE
  | inline x : TYPE
  | TYPE x : TYPE
  | out TYPE x : TYPE
  | inout TYPE x : TYPE

PRETS ::= PRET , ... , PRET
<a href="#parameters">PRET</a> ::=
  | ghost x : TYPE
  | TYPE x : TYPE

SPECS ::= SPEC ... SPEC
SPEC ::=
  | reads x ; ... ; x ;
  | modifies x ; ... ; x ;
  | requires LEXP ; ... LEXP ;
  | ensures LEXP ; ... LEXP ;
  | requires / ensures LEXP ; ... LEXP ;

LEXP ::=
  | EXP
  | let FORMAL := EXP

STMTS ::= STMT ... STMT
STMT ::=
  | assume EXP ;
  | assert EXP ;
  | assert EXP by { STMTS }
  | calc <i>[</i>CALCOP<i>]</i> { CALC ... CALC }
  | reveal f ;
  | p ( EXP , ... , EXP) ;
  | ASSIGN ;
  | <i>[</i>ghost<i>]</i> var x <i>[</i>: TYPE<i>]</i> <i>[</i>:= EXP<i>]</i> ;
  | forall FORMALS TRIGGERS <i>[</i>:| EXP<i>]</i> :: EXP { STMTS }
  | exists FORMALS TRIGGERS :: EXP ;
  | while ( EXP ) INVARIANTS DECREASE { STMTS }
  | for ( ASSIGNS ; EXP ; ASSIGNS ) INVARIANTS DECREASE { STMTS }
  | <i>[</i>ghost<i>]</i> <i>[</i>inline<i>]</i> if ( EXP ) { STMTS }
    <i>[</i> else if ( EXP ) { STMTS } ... else if ( EXP ) { STMTS } <i>]</i>
    <i>[</i> else { ... } <i>]</i>

CALC ::=
  | <i>[</i>CALCOP<i>]</i> EXP ;
  | <i>[</i>CALCOP<i>]</i> { STMTS }
CALCOP ::= &lt; | &gt; | &lt;= | &gt;= | == | &amp;&amp; | || | &lt;== | ==&gt; | &lt;==&gt;

ASSIGNS ::= ASSIGN , ... , ASSIGN
ASSIGN ::= 
  | x <a href="#overloading">POSTFIX_OP</a>
  | x := EXP
  | this := EXP
  | DESTINATIONS := p ( EXP , ..., EXP )

DESTINATIONS := DESTINATION <i>[</i> , ... , DESTINATION <i>]</i>
DESTINATION ::=
  | x
  | ( <i>[</i>ghost<i>]</i> var x <i>[</i>: TYPE<i>]</i> )

INVARIANTS ::= INVARIANT ... INVARIANT
INVARIANT ::= invariant EXP ; ... EXP ;

DECREASE ::=
  | decreases * ;
  | decreases EXP <i>[</i>, ... , EXP <i>]</i> ;

TRIGGERS ::= TRIGGER ... TRIGGER
TRIGGER ::= { EXP <i>[</i> , ... , EXP <i>]</i> }

EXP ::=
  | x
  | f
  | true | false
  | 0 | 1 | 2 | 3 | ... | 1_000_000 | ...
  | 0.1 | 0.2 | ... | 3.14159 | ...
  | 0x0 | 0x1 | ... | 0xdeadBEEF | 0x1_0000_0000 | ...
  | bv1(0) | bv32(0xdeadbeef) | bv64(7) | ...
  | "STRING"
  | ( - EXP )
  | this
  | @x
  | const(EXP)
  | f ( EXP , ... , EXP )
  | EXP [ EXP ]
  | EXP [ EXP := EXP ]
  | EXP ?[ EXP ]
  | EXP . fd
  | EXP . ( fd := EXP )
  | old ( EXP )
  | old [ EXP ] ( EXP )
  | seq ( EXP , ... EXP )
  | set ( EXP , ... , EXP )
  | list ( EXP , ... , EXP )
  | tuple ( EXP , ... , EXP )
  | ! EXP
  | EXP * EXP | EXP / EXP | EXP % EXP
  | EXP + EXP | EXP - EXP
  | EXP &lt; EXP | EXP &gt; EXP | EXP &lt;= EXP | EXP &gt;= EXP | EXP is c
  | EXP == EXP | EXP != EXP
  | EXP &amp;&amp; EXP
  | EXP || EXP
  | EXP &lt;== EXP | EXP ==&gt; EXP
  | EXP &lt;==&gt; EXP
  | if EXP then EXP else EXP
  | let FORMAL := EXP in EXP
  | forall FORMALS TRIGGERS :: EXP
  | exists FORMALS TRIGGERS :: EXP
  | lambda FORMALS TRIGGERS :: EXP
  | ( EXP )

TYPE ::=
  | t
  | TYPE ( TYPE , ... , TYPE )
  | tuple ( TYPE , ... , TYPE )
  | ( TYPE )
    </pre>
    </td>
    <td>
    <pre>
---


function f(x:int, y:int):bool
      

procedures p(ghost x:int) returns(ghost y:int)
  requires
    0 &lt;= x;
    isEven(x);
  ensures 
    x &lt;= y;
{ ... }


assume x &lt; 10;
assert x &lt;= 10;
assert x &lt;= 10 by { myLemma(x); }
calc { x; x * 1; { myLemma(x); } 1 * x; }
reveal myOpaqueFunction;
Increment(x);
x := 5;
ghost var x:uint32 := 33 + 44;
forall x:int, y:int :| x &lt; y :: x &lt;= y { ... }
exists x:int :| 0 &lt;= x;
while (eax != 0) invariant true; decreases *; { ... }
for (eax := 0; eax < 10; eax++) decreases eax; { ... }
if (eax != 5) { Increment(edx) } else { eax := 0; }


x++;


eax, (ghost var x:int), y := myProc(ebx, edx, z);


m?[10] // Dafny only; like Dafny's "10 in m"


old(x)
old[snapshotOfThis](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:
|
|   *, /, % have highest precedence   
|
|   all binary operators are left-associative
|   except for ==&gt;, which is right-associative
|
|   &lt;==&gt; has lowest precedence

let x := 3 in x + 1
forall x, y {foo(x, y)} :: foo(x, y) || x == y


uint32
map(int, set(uint32))
tuple(int, int, bool)
---
    </pre>
    </td>
    </tr>
    </table>

  <h3 id="verbatim">Verbatim blocks</h3>
  <p>
    Vale programs may contain verbatim blocks (VERBATIM_DECL_BLOCK in the table above):

    <pre><code>
      #verbatim
      method printCode(...) { ... }
      lemma L(...) { ... }
      #endverbatim

      procedure p()
      {
        L(...);
        ...
      }

      #verbatim
      method Main()
      {
        printHeader();
        var n := printCode(va_code_p(), 0);
        printFooter();
      }
      #endverbatim
    </code></pre>

  <p>
    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.

  <h3 id="attributes">Attributes</h3>

  <p>
    Some elements of the Vale grammar may be annotated with <i>attributes</i>
    that supply additional information to Vale or to the verification language.
    Currently, attributes are only supported in the following places:
    
  <p>
    <table border="1">
      <tr><td>Grammar (attributes)</td></tr>
      <tr>
      <td>
      <pre>
INCLUDE ::= include ATTRIBUTES "STRING"

DECL ::=
  ...
  | var ATTRIBUTES x : TYPE ;
  | procedure ATTRIBUTES p ( ... ) ...
  ...

ATTRIBUTES ::= ATTRIBUTE ... ATTRIBUTE
ATTRIBUTE ::= {: x EXP , ... , EXP }
      </pre>
      </td>
      </tr>
    </table>

    Currently, the following attributes are supported:
    <ul>
      <li>{:verbatim} on include directives, which directs Vale to include a file written directly in the underlying verification language, rather than including another Vale file</li>
      <li>{:instruction EXP} on procedures, indicating a primitive procedure that is implemented with the code value specified by the expression EXP</li>
      <li>{:operand} on procedures, indicating an operand constructor</li>
      <li>{:state f(EXP, ..., EXP)} on global variable declarations, indicating that the variable x corresponds to a field f(EXP, ..., EXP) of the state type.</li>
      <li>{:refined} and {:bridge} on procedures -- an experimental feature that uses a more complicated, but sometimes more efficient, Dafny encoding for generated lemmas</li>
    </ul>

  <h2 id="procedures">Procedures</h2>

  <p>
    Vale procedures consist of parameter and return value declarations,
    specifications (requires and ensures),
    and a body containing statements.
    Parameters, return values, and statements may be <i>physical</i> or <i>ghost</i>.
    Physical entities correspond to runnable code,
    while ghost entities exist only to assist proving that code meets its specifications.

  <p>
    While loops and for loops are always physical.
    If/else statements may be physical or ghost.
    Procedure calls, variable declarations, assignments may be physical or ghost.
    Assume, assert, reveal, forall, and exist statements are always ghost.
    Statements inside forall statements and ghost if/else statements must be ghost statements.

  <p>
    Currently, all procedures declared with a Vale "procedure" declaration
    are assumed to be physical,
    while procedures declared outside Vale (in Dafny, F*, or Lean)
    are assumed to be ghost.

  <h3 id="state">Variables, expressions, and state</h3>

  <p>
    Ghost parameters, ghost variables, ghost statements, and ghost procedure calls
    are translated almost directly into their corresponding verification language constructs.
    Ghost expressions may, however, refer to physical variables,
    and the translation of references to physical variables depends on Vale's notion of state.
    For example, if the physical variable "eax" represents an assembly language register,
    then the expression "eax == 0" means that the register eax is zero in the current state.

  <p>
    In Vale, the current state is always named "this", which has type va_state.
    Values of the state type are considered ordinary ghost values and may be stored in
    ghost variables, passed as ghost arguments, and so on.
    For example, the statement "ghost x := this;" saves a copy of the current state in variable x.
    By default, all expressions are evaluated with respect to the current state "this".
    However, the expression old(e) evaluates the expression e in the state
    at the beginning of a procedure's execution;
    this is often useful for specifying how state changes during procedure execution.
    For example, the specification "ensures eax == old(eax) + 1;" says that a procedure
    execution must increase the value stored in eax by 1.
    Occasionally, it is also useful to write an assertion comparing two states inside a procedure.
    For this, the expression old[e1](e2) evaluates e2 in state e1.
    For example, this code saves a copy of the state at the beginning of a loop iteration,
    and then asserts that eax at the end of the loop iteration equals the value at
    the beginning of the loop iteration plus 1:

    <pre><code>
      procedure p(...) ...
      {
        ...
        while (eax != 10) ...
        {
          ghost var savedThis := this;
          ...
          assert eax == old[savedThis](eax) + 1;
        }
        ...
      }
    </code></pre>

  <h3 id="physicalVars">Declaring global state variables</h3>

  <p>
    Vale programs view the state by declaring "state variables" that represent
    fields (components) of the state:

    <pre><code>
      var{:state ok()} ok:bool;
      var{:state reg(EAX)} eax:int;
      var{:state reg(EBX)} ebx:int;
      var{:state flags()} efl:int;
    </code></pre>

  <p>
    Vale translates a reference to a state variable, such as eax or flags,
    into an accessor function call, such as va_get_reg(EAX, this) or va_get_flags(this).
    The definition of the state, the state variables, and the state accessor
    functions is up to the programmer (see the <a href="#interface">Vale interface</a> section).
    However, Vale requires a state variable named "ok" of type bool to represent
    a good state (ok == true) or a failed state (ok == false).
    Also, it is recommended that different state variables represent independent portions
    of the state (no overlap between variables); in fact, the experimental "{:refined}" attribute requires this.

  <h3 id="parameters">Procedure parameters and return values</h3>

  <p>
    Procedure parameters and returns values may be operands, inline, or ghost:
    <ul>
      <li>Operand parameters and return values are physical variables whose value depends on the state at run-time.</li>
      <li>Inline parameters are physical variables whose value does not depend on the state.
          Arguments to inline parameters may be arbitrary functions of other inline parameters,
          but may not depend on "this".</li>
      <li>Ghost parameters and ghost return values are ghost variables whose value may depend on the state.</li>
    </ul>

  <p>
    Operand parameters are either "in", "out", or "inout".
    Operand return values are always considered "out".
    For parameters, the default is "in", while "out" parameters and "inout" parameters are marked
    with the keywords "out" and "inout":

    <pre><code>
      procedure Move(out register dst:int, operand src:int)
      procedure Increment(inout register dst:int)
    </code></pre>

  <p>
    Each operand parameter or return value has two types, an operand type and a value type.
    In the example above, "dst" has operand type "register" and value type "int".
    The operand type describes the type used to represent the operand in code values and lemmas.
    Programmers may declare as many operand types as they wish
    (see the <a href="#interface">Vale interface</a> section for details).
    For example, different operand types might be used to represent register operands,
    memory operands, floating-point operands, or combinations of these.
    References to an operand like "dst" will have the that operand's value type (such as int).
    For example, the expression "dst + src" in the example below will add an int to another int.
    For any operand x, the expression @x refers to the operand itself rather than the value
    stored in the operand.  The expression @dst, for example, has type va_register rather than int,
    and @src has type va_operand rather than int.

  <p>
    For any operand type O and value type t,
    the accessor function va_eval_O_t(s:va_state, o:va_O).
    In the following example, Vale translates the expression
    dst + src into
    va_eval_register_int(this, @dst) + va_eval_operand_int(this, @src):

    <pre><code>
      procedure Add(inout register dst:int, operand src:int)
        requires
          dst + src &lt; 0x1_0000_0000;
        ensures
          dst = old(dst + src);
      { ... }

      procedure p2() ...
      {
        Add(eax, ebx); // instantiate Add with destination eax and source ebx
        Add(ebx, eax); // instantiate Add with destination ebx and source eax
        Add(eax, 7);   // instantiate Add with destination eax and source 7
        Add(eax, const(2 + 2));   // instantiate Add with destination eax and source 4
        assert eax == old(eax + ebx) + 11;
      }
    </code></pre>

  <p>
    Operand parameters may be instantiated with constants, state variables, operands, or operand constructor applications.
    Operand return values may be instantiated with state variables, operands, or operand constructor applications.
    Constants passed as operand parameters may either be simple integer literals,
    or more complex expressions inside a "const(...)" expression.

  <h2 id="overloading">Operator overloading</h2>

  <p>
    To allow Vale programs to use familiar C-like notation,
    Vale allows user-defined operators.
    Vale programs can define new operator tokens
    constructed from the following characters:
    <pre><code>
      ! % + - * &amp; ^ | &lt; &gt; = . # : $ ? ` ~ @
    </code></pre>

  <p>
    New operators must be distinct from Vale built-in operators, which are:
    <pre><code>
      @ . : :| ::
      ! * / % + - &lt; &gt; = := &lt;= &gt;= == != &amp;&amp; || &lt;== ==&gt; &lt;==&gt;
    </code></pre>

  <p>
    The "#token" declaration introduces a new token and gives it a precedence and associativity equal
    to the precedence and associativity of a user-chosen builtin operator:

    <pre><code>
      #token ++ precedence !
      #token += precedence :=
    </code></pre>

  <p>
    In this example, "+=" is declared to have the same precedence as ":=",
    and "++" is declared to have the same precedence as "!".

  <p>
    For infix operators, any of these operators may be used to indicate precedence:
    <pre><code>
      * / % + - &lt; &gt; = := &lt;= &gt;= == != &amp;&amp; || &lt;== ==&gt; &lt;==&gt;
    </code></pre>

  <p>
    For postfix operators, the "!" is used to indicate precedence.

  <p>
    Vale programs can overload user-defined tokens and the builtin ":=" token
    to represent procedures:

    <pre><code>
      procedure Mov(...) ... { ... }
      procedure Add(...) ... { ... }
      procedure Increment(...) ... { ... }

      procedure operator(:=) (out operand dst:int, operand src:int) := Mov
      procedure operator(+=) (inout operand dst:int, operand src:int) := Add
      procedure operator(++) (inout operand dst:int) := Increment
    </code></pre>

  <p>
    This example defines three procedure operators: ":=" as an alias for the Mov procedure,
    "+=" as an alias for the Add procedure, and "++" as an alias for the Increment procedure.

  <p>
    Procedure operators only act on physical variables, not ghost variables
    (see <a href="#procedures">procedures</a>
    for more information about physical variables and ghost variables).
    For example, "x += 5;" means "Add(x, 5);" if x is a physical variable,
    but is not defined if x is a ghost variable.

  <p>
    Procedure operators for a user-defined infix token OP must be declared
    to have two parameters, the first inout and the second in, and no return values.
    Such an operator may only be used in a statement of the form "x OP EXP;".

  <p>
    Procedure operators for a user-defined postfix token OP must be declared
    to have one inout parameters and no return values.
    Such an operator may only be used in a statement of the form "x OP;".

  <p>
    Procedure operators for ":=" must either have one out parameter followed by
    one in parameter (with no return values), or one in parameter and one return value.
    Overloading the ":=" operator only affects statements of the form "x := EXP;"
    where x is a physical variable and EXP is not a procedure call;
    other uses of ":=" are unaffected.

  <h2 id="interface">Interface between Vale and verification languages</h2>

  <p>
    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:

    <ul>
      <li>
        In Dafny, all Vale-generated names begin with
        the prefix "va_".  Hand-written Dafny code should avoid names beginning with "va_"
        if the hand-written code will be linked with the Vale-generated code.
      </li>
    </ul>

  <p>
    Each procedure with name p generated by Vale becomes a function named
    "va_code_" concatenated with p.
    In addition, Vale generates a lemma for each procedure named
    "va_lemma_" concatenated with p.

  <p>
    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".

  <h3 id="library">Vale library</h3>

  <p>
    When Vale generates code in the chosen verification language (Dafny, FStar, etc.),
    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.

  <p>
    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,
    and the names "va_bool" and "va_int" are assumed to be aliases for Dafny's
    built-in boolean and mathematical integer types "bool" and "int".
    Types written as "..." are unconstrained by Vale and may be chosen by the library.
    The symbols "t" and "O" refer to value types and operand types.
    A special operand type O = "cmp" is used for conditionals in if/else and while/for statements.

    <ul>
      <li>Types: bool, int, state, code, codes, O</li>
      <li>Lemmas: lemma_ifElse, lemma_while, lemma_whileTrue, lemma_whileFalse, lemma_whileInv, lemma_empty, lemma_block</li>
      <li>Functions:
        <ul>
          <li>CNil():codes</li>
          <li>CCons(hd:code, tl:codes)</li>
          <li>eval_O_t(s:state, o:O):t</li>
          <li>const_O(n:int):O</li>
          <li>require(b0:codes, c1:code, s0:state, sN:state):bool</li>
          <li>ensure(b0:codes, b1:codes, s0:state, s1:state, sN:state):bool</li>
          <li>state_eq(s0:state, s1:state):bool</li>
          <li>is_src_O_t(o:O):bool</li>
          <li>is_dst_O_t(o:O):bool</li>
          <li>update_O(o:O, sM:state, sK:state):state</li>
          <li>Accessor functions for state fields f:
            <ul>
              <li>op_O_f(...):O</li>
              <li>get_f(..., s:state):t</li>
              <li>update_f(..., sM:state, sK:state):state</li>
            </ul>
          </li>
          <li>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.)
          </li>
          <li>get_block(c:code):codes</li>
          <li>get_ifCond(c:code):cmp</li>
          <li>get_ifTrue(c:code):code</li>
          <li>get_ifFalse(c:code):code</li>
          <li>get_whileCond(c:code):cmp</li>
          <li>get_whileBody(c:code):code</li>
          <li>whileInv(b:cmp, c:code, n:int, r1:state, ok1:bool, r2:state, ok2:bool):bool</li>
          <li>IfElse(cond:cmp, ift:code, iff:code):code</li>
          <li>While(cond:cmp, body:code):code</li>
          <li>Block(block:codes):code</li>
        </ul>
      </li>
    </ul>

</body>
</html>