Implementation

Main stages in going from program to verification result:

annotated program 
-> type checking with Mypy -> parsing with OCamllex and Menhir
-> operations on Python AST -> translation to Dafny AST -> printing of Dafny AST 
-> running verifier -> reporting results

Position Information

During lexing, position information is stored for every operator, identifier and type. This information is then stored together with a token's value (if applicable) as a segment, as part of an AST node.

type pos = { pos_lnum : int ; pos_bol : int ; pos_cnum : int }
type segment = pos * string option

• pos_lnum corresponds to the line number
• pos_bol corresponds to the number of characters from the beginning of the lexer buffer to the beginning of the line
• pos_cnum corresponds to the number of characters from the beginning of the lexer buffer to the current position.

The column number can be obtained by subtracting pos_bol from pos_cnum, when reporting an error to the user for example.

Lists

Supporting lists has the following requirements:

• Mutability
• Methods, such as append
• Primitive operations, such as + which is used to concatenate two lists (yet to be supported)

While Dafny supports arrays which are mutable, their operations do not correspond to lists in Python. As such, lists are supported via the following:

1. a list class specified in Dafny
2. rewriting lists to make use of the specified list class Currently, lists are the only mutable data structure supported. Support for other data structures can be added in a similar manner.

Here is the complete list specification

List Class

The list class specifies a generic parameter for its elements and internally makes use of a sequence to store them. It supports all methods of Python’s list class except for sort. In the case of sort, since the elements are of a generic type, a general comparison function cannot be used. Where possible, preconditions are specified in order to restrict the possible uses. For instance, the pop method specifies that the length of the list should be greater than one so that a verification will be raised if it is not:

method pop() returns (popped: T)
  requires |lst| > 0
  modifies this
  ensures lst == old(lst)[0..|old(lst)| - 1] ensures popped == old(lst)[|old(lst)| - 1]
{
  popped := lst[|lst| - 1];
  lst := lst[0..|lst| - 1]; 
}

Rewriting Lists

In rewriting Python lists to correspond to the Dafny list class, the following operations are performed:

1. for every literal list such as [1, 2, 3], an assignment statement is created whose right-hand expression is a call to the list constructor. The literal list is then replaced with the assignment’s identifier
2. subscripts are converted to their corresponding to method call in the list class [0..3] would be converted to .range(0, 3)
3. the Python built-in function len is converted to the len method of the list class. len([1, 2, 3]) would be converted to [1, 2, 3].len().

Primitive Operations

To extend primitive operation support for datastructures, type inference can be used to recognize recognize these operations involving datastructures and rewrite them accordingly. This remains to be implemented.

Built-Ins

Together with the translated user program, a set of functions specified in Dafny is also appended before the Dafny verifier is executed. These functions correspond to built-in functions in Python and enables them to be incorporated as part of the verification process. Currently, map and filter are supported.

Here are the built-in specifications

Type Variables

Python:

from typing import TypeVar
T = TypeVar("T")
# reads l
# pre len(l) > 0
# post res1 == l[0]
def first(l: list[T]) -> T:
  return l[0]

Dafny:

function method first<T>(l: list<T>): (res1: T)
  reads l
  requires (l.len() > 0)
  ensures (res1 == l.atIndex(0)) 
{
  l.atIndex(0) 
}

Assumptions:

• type variables are only declared at the top level of the program
• all functions make use of any declared type variables

Type variables are supported via Dafny’s generic types. All top level assignment statements are checked for whether their assignment target is a call expression declaring a type variable, obtaining a list of type variables in the entire program. All Dafny functions are then parameterized with all the variables in the list.

Type Synonyms

Python:

ConnectionOptions = dict[str, str]
Address = tuple[int, int]
Server = tuple[Address, Address]

Dafny:

type ConnectionOptions = map<string, string>
type Address = (int, int)
type Server = (Address, Address)

A type synonym declaration can be recognized by checking the right-hand-side of an as- signment. Their identifiers are stored in a set of strings. All assignments are then checked for whether their right-hand-side contains any such identifier. If so, the assignment is assumed to be a type synonym declaration and converted appropriately to Dafny.

Function Calls in Specifications

# post res == x
def f(x: int) -> int: 
  return x

i = 10
# invariant 0 <= i and i <= 10 
# invariant i == f(i)
while 0 < i:
  i=i-1

This is a limitation imposed by Dafny which does not support methods in specifications. To mitigate this, functions which contain a single return statement or expression are translated to Dafny function methods instead, which can be used in specifications. This is done by pattern matching on the bodies of all functions in the program.

Otherwise, functions are not supported in specifications.

Function Calls in Expressions

method one() returns (res: int)
    ensures res == 1
{
  return 1;
}
method call_one() {
  var a := 10 * one();
}

Such calls are not supported by Dafny. To support them, the following rewriting rules are used:

1. insert an assignment statement immediately before the statement in which the expression occurs and whose right-hand side is the method call
2. replace the method call in the expression context with the identifier of the new assignment inserted in 1.