Dafny tutorial

What's new in Dafny?
And what is Dafny, anyway?

Tutorial outline

• Dafny as a programming language
• Dafny as more than a programming language
• Dafny as a proof assistant
• Verification of programs in Dafny

More than the tutorial abstract promised!

Virtues of Dafny

• Write programs and prove them correct
• Interface with multiple other languages
• Write models and proofs

Some uses of Dafny

• AWS Encryption SDK
• AWS Database Encryption SDK
• Cedar authorization policy language used by Amazon Verified Permissions and AWS Verified Access
• VeriBetrFS
• Etherium VM interpreter
• DaisyNFS
• Ironclad, IronFleet, Vale, Armada

Teaching using Dafny

• At tens of universities worldwide for over a dozen years
• New book: Program Proofs (MIT Press)

Programming language

• Imperative features
  • :=, if, while, class, new, method
• Functional features
  • function, datatype, match
• Specification features
  • preconditions, termination metrics
• Proof-authoring features
  • assertions, lemmas, proof calculations

Intergrated Development Envionment

• VS Code (recommended)
  • Install VS Code
  • Install Dafny extension
  • Create file with extension .dfy
• Emacs
• Command-line interface

Hello World

method Main() {
  print "hello, Dafny\n";
}

• Demo
  • dafny run Hello.dfy

Methods

method SimpleMethod(x: int, b: bool) {
  var y := x + 3;
  print y, " ", b, "\n";
}

method MethodWithResults(x: int) returns (r: int, s: int) {
  r := x;
  s := x + 3;
}

Functions

function MyFunction(x: int, b: bool): int {
  x + 3
}

predicate IsInstructor(name: string) {
  name == "Rustan"
}

Types

• built-in types (bool, int, …)
• type T = U (type synonym)
• type T (abstract type)
• datatype
• codatatype
• newtype
• class
• trait
• type T = u: U | P(u) (subset type)

Built-in types

BuiltinType ::=
  // primitive types
  | bool | int | real | char
  | bv0 | bv1 | bv2 | ...
  | object
  | ORDINAL
  // collection types
  | set<Type> | iset<Type> | multiset<Type>
  | seq<Type>
  | map<Type, Type> | imap<Type, Type>
  // arrow types
  | () -> Type | (Type) -> Type | (Type, Type) -> Type | ...
  | () --> Type | (Type) --> Type | (Type, Type) --> Type | ...
  | () ~> Type | (Type) ~> Type | (Type, Type) ~> Type | ...
  // tuple types
  | () | (Type, Type) | (Type, Type, Type) | ...
  // array types
  | array<Type> | array2<Type> | array3<Type> | ...
  // others
  | nat | string

About types

• Dafny is type safe: Every use of a variable is guaranteed to get a value of the variable's type
• Types are nominal
• Types may be empty
• Polymorphism
  • is parametric
  • is predicative
• Traits, datatypes, newtypes, classes, and abstract types can have members

Booleans

• false, true
• !
• &&, ||
  • short-circuiting
• ==>, <==
  • short-circuiting
• <==>
• Wider operators have lower binding power
  • A && B ==> C && D means the same thing as
    (A && B) ==> (C && D)

Quantifiers

predicate HasMimimum(s: set<int>) {
  exists m ::
    m in s &&
    forall x :: x in s ==> m <= x
}

TLA+-style bullets for && and ||

predicate IsIndexOfMinimum(i: int, s: seq<int>) {
  && 0 <= i < |s|
  && forall j :: 0 <= j < |s| ==> s[i] <= s[j]
}

• Note that whitespace is not significant, so you may still need parentheses

predicate BadBullets(A: bool, B: bool, C: bool, D: bool) {
  && A
  && B ==> C  // warning: did you forget parentheses?
  && D
}

Integers

• unbounded
• literals can separate digits with _
  • 800_555_1212
  • 0x8000_0000
• Euclidean div and mod
• comparison operators are chaining
  • 0 <= i < j < 100
• type nat = x: int | 0 <= x
• bounded integers can be defined using newtype

Reals

• 2.0, 37.2
• unbounded
• no floating-point support

Characters

• 'D', '\n', '\U{10_aBcD}'
• Unicode
• type string = seq<char>

Bitvectors

• available in any width
  • not polymorphic in width
• &, |, ^
• <<, >>
• .RotateLeft, .RotateRight
• arithmetic operations treat bitvectors like unsigned integers with modulo arithmetic

Wider operators have lower binding power

Newtypes

newtype MyInt = int
newtype int32 = x: int | -0x8000_0000 <= x < 0x8000_0000
newtype byte = x | 0 <= x < 256

newtype Primes = x | IsPrime(x)
predicate IsPrime(x: int) {
  2 <= x && forall y :: 2 <= y < x ==> x % y != 0
}

• (“derived types” in Ada)
• The purpose of a newtype is to define a type that is separate from the base type, but with the values and operations (possibly constrained) of the base type
• The value of all (sub)expressions of the newtype must satisfy the constraint
• A newtype gives the compiler the freedom to represent the type and its base type differently
• Compiles to native words, when possible

Type inference

method Examples() {
  var a: int;
  var b: int32;
  var c: bv32;
  a := 25;
  b := 25;
  c := 25;
  var d := 25;
  var e;
  e := 25 as int32;
}

Sets

method Combine(a: set<real>, b: set<real>)
  returns (c: set<real>)
{
  c := a + b;
  assert |c| <= |a| + |b|;
  c := c + {2.0, 37.2};
}

• Sets are crucial for frame specifications (used with mutable objects in the heap)

Sequences

method Shuffle(s: seq<char>) returns (r: string) {
  var n := |s| / 2;
  r := s[n..] + ['a', 'b', 'c'] + s[..n] + "xyz";
  var c := r[5];
  r := r[2..6];
}

Comprehensions

method Squares(n: nat) {
  // set of first n natural numbers:
  var s := set i | 0 <= i < n;
  // set of first n squares:
  var t := set i | 0 <= i < n :: i * i;
  // map from first n natural numbes to their squares:
  var m := map i | 0 <= i < n :: i * i;
  // map to first n natural numbes from their squares:
  var w := map i | 0 <= i < n :: i * i := i;
  // sequence of first n squares:
  var q := seq(n, i => i * i);
}

Datatypes

datatype List<X> = Nil | Cons(head: X, tail: List<X>)
datatype Rainbow = L | G | B | T | Q | I | A
datatype Expr =
  | Const(value: int)
  | Variable(string)
  | Plus(0: Expr, 1: Expr)
datatype Record = Record(name: string, age: nat)

• first | is optional
• parentheses after nullary constructors can be (and typically are) omitted
• constructor parameters can be given names
• such names can look like numeric literals
• constructor can have same name as the type

Match

method Print(expr: Expr) {
  match expr
  case Const(value) =>
    print value;
  case Variable(name) =>
    print name;
  case Plus(left, right) =>
    Print(left);
    print " + ";
    Print(right);
}

It is an error if a match is reached and no case applies

Discriminators and destructors

method Print(expr: Expr) {
  if expr.Const? {
    print expr.value;
  } else if expr.Variable? {
    var Variable(name) := expr;
    print name;
  } else {
    Print(expr.0);
    print " + ";
    Print(expr.1);
  }
}

Datatype update

method Double(expr: Expr) {
  if expr.Const? {
    var u := expr.(value := 2 * expr.value);
  }
}

Wrapper classes

datatype Macklemore = Macklemore(rhyme: string)

Simple wrapper constructors are compiled away

Tuples

Tuple types are built-in, anonymous datatypes

// If you wrote them yourself, you'd write:
datatype Tuple0 = Tuple0()
datatype Tuple2<X, Y> = Tuple2(0: X, 1: Y)
datatype Tuple3<X, Y, Z> = Tuple3(0: X, 1: Y, 2: Z)
// ...

// The built-in ones have this special syntax:
datatype () = ()
datatype (X, Y) = (0: X, 1: Y)
datatype (X, Y, Z) = (0: X, 1: Y, 2: Z)
// ...

Intermezzo

Trivia question:

Dafny has two built-in unit types (that is, types with exactly one value). What are they?

Codatatypes

A codatatype represents possibly infinite structures

codatatype Stream<X> = Next(head: X, tail: Stream<X>)
codatatype DeepTree<X> =
  | Leaf
  | Node(left: DeepTree<X>, value: X, right: DeepTree<X>)

Subset types

(aka “refinement types” or “predicate subtypes”)

type Even = x: int | x % 2 == 0

method Examples(x: Even, i: int) {
  var y: Even := (1 + x) + 1;
  if i % 2 == 0 {
    var z: Even := i;
  }
}

Subset types

datatype IntList =
  | End(value: int)
  | Point(value: int, next: IntList)

predicate IsIncreasing(ii: IntList) {
  ii.Point? ==>
    && ii.value <= ii.next.value
    && IsIncreasing(ii.next)
}

type IncreasingList = ii: IntList | IsIncreasing(ii)

Typical naming

datatype IncreasingList_ =
  | End(value: int)
  | Point(value: int, next: IncreasingList_)

predicate Valid(ii: IncreasingList_) {
  ii.Point? ==>
    && ii.value <= ii.next.value
    && Valid(ii.next)
}

type IncreasingList = ii: IncreasingList_ | Valid(ii)

Using a member function

datatype IncreasingList_ =
  | End(value: int)
  | Point(value: int, next: IncreasingList_)
{
  predicate Valid() {
    Point? ==>
      && value <= next.value
      && next.Valid()
  }
}

type IncreasingList = ii: IncreasingList_ | ii.Valid()

Classes

class Cell {
  var data: int
}

class Person {
  const name: string
  var age: nat

  constructor (name: string, age: nat) {
    this.name := name;
    this.age := age;
  }

  constructor Newborn(name: string) {
    this.name := name;
    age := 0;
  }
}

method Client() {
  var c := new Cell;
  c.data := 17;

  var p0 := new Person("Manilow, Barry", 80);
  var p1 := new Person.Newborn("Mumford, Sunny");
}

Using the object being constructed

class Cell<X> {
  var data: X
  var usageLog: seq<string>

  constructor (x: X) {
    usageLog := [];
    AppendToLog("creation"); // not allowed
    data := x;
  }

  method AppendToLog(event: string) {
    usageLog := usageLog + [event];
  }
}

Two-phase constructors

class Cell<X> {
  var data: X
  var usageLog: seq<string>

  constructor (x: X) {
    usageLog := [];
    data := x;
    new;
    AppendToLog("creation");
  }

  method AppendToLog(event: string) {
    usageLog := usageLog + [event];
  }
}

Example: Initializing a cyclic list

class CyclicList<X> {
  var data: X
  var next: CyclicList<X>

  constructor (x: X) {
    data := x;
    next := this;
    new;
  }

  method Merge(that: CyclicList<X>) {
    this.next := that;
    that.next := this;
  }
}

Non-null reference types

Every reference type, for example

class Cell { /*...*/ }

gives rise to two types:

• Cell? is a nullable type, consisting of the allocated Cell objects and the value null
• Cell is the corresponding non-null type, defined automatically as a subset type:

type Cell = c: Cell? | c != null

Arrays

method Arrays() {
  var arr: array<int>;
  var matrix: array2<real>;
  arr := new int[25];
  matrix := new real[100, 20];
  arr[3] := 123;
  matrix[4, 5] := 3.75;
}

Array operations

method Squares(n: nat) returns (s: seq<int>) {
  var arr := new int[n](i => i * i);
  s := arr[0..arr.Length];
  s := arr[..arr.Length];
  s := arr[0..];
  s := arr[..];

  arr := new int[3] [2, 3, 5];
  arr := new int[] [2, 3, 5];
  arr := new [] [2, 3, 5];
}

Traits

trait Animal extends object {
  const name: string
  var age: nat
  method Print()
}
class Tiger extends Animal {
  constructor (firstName: string) {
    name := firstName + " the Tiger";
    age := 0;
  }
  method Print() {
    print name, " is ", age, " years old\n";
  }
}

Traits for reference types

• In the current version of Dafny (version 4.1), all traits are reference types
• This is changing. Soon, Dafny will also support non-reference-type traits, so that datatypes, newtypes, and abstract types can extend traits, too.

Expressions and Statements

Dafny distinguishes between expressions and statements, and, in an analogous way, between functions and methods.

In most cases, syntax of corresponding expression/statement constructs are the same. (Exception: ternary if-then-else expression versus if statement.)

Let bindings and local variables

function Triple(x: int): int {
  var double := x + x;
  x + double
}

method MTriple(x: int) returns (r: int) {
  var y := 4 * x;
  y := y + 2 * x;
  r := y / 2;
}

Match expression/statement

function Length<X>(list: List<X>): nat {
  match list
  case Nil => 0
  case Cons(_, tail) => 1 + Length(tail)
}

method MLength<X>(list: List<X>) returns (len: nat) {
  match list
  case Nil =>
    len := 0;
  case Cons(_, tail) =>
    len := MLength(tail);
    len := len + 1;
}

Conditional constructs

function Length<X>(list: List<X>): nat {
  if list == Nil then
    0
  else
    1 + Length(list.tail)
}
method MLength<X>(list: List<X>) returns (len: nat) {
  if list == Nil {
    len := 0;
  } else {
    len := MLength(list.tail);
    len := len + 1;
  }
}

Recursion vs iteration

function Length<X>(list: List<X>): nat
  // auto-accumulator tail-recursive function
{
  if list == Nil then
    0
  else
    1 + Length(list.tail)
}
method MLength<X>(list: List<X>) returns (len: nat) {
  len := 0;
  var xs := list;
  while xs != Nil {
    len := len + 1;
    xs := xs.tail;
  }
}

Match patterns

function NestedPattern(list: List<int>): int {
  match list
  case Nil => 0
  case Cons(5, _) => 1
  case Cons(x, Nil) => 2 + x
  case Cons(_, Cons(7, _)) => 3
  case _ => 4
}
function DisjunctivePattern(rainbow: Rainbow): int {
  match rainbow
  case L => 0
  case G | B => 1
  case _ => 2
}

Return

method M(x: int, y: int) returns (r: int, s: int) {
  r := x + y;
  if x < y {
    r := r + 5;
  } else if x == 100 {
    s := 10;
    return;
  } else {
    return r + 5, 10;
  }
  s := 10;
}

Calls

function F(x: int): (bool, real)
method M(x: int) returns (b: bool, r: real)

method Caller() {
  var pair: (bool, real);
  var b: bool;
  var r: real;
  pair := F(10);
  b, r := M(10);
  var (bb, rr) := F(10);
}

Identifiers

• identifiers can include _, ', and ?
• user-defined identifiers cannot start with _
• some identifiers are allowed to look like integer literals

Combining declaration and assignment

• typically, you can declare a variable (var) and assign it at the same time
• this applies to calls and assignments :=, :|, :-

method Examples() {
  var x;
  x := 10;

  var y := 10;
}

Variables and parameters

• in-parameter cannot be changed in body
• but you can shadow an in-parameter with a mutable local variable

method MLength<X>(list: List<X>) returns (len: nat) {
  len := 0;
  var list := list;
  while list != Nil {
    len := len + 1;
    list := list.tail;
  }
}

Simultaneous assignment

method Simultaneous() returns (r: int) {
  var i, v: bv32, b := 0, 0, true;
  var j;
  i, j := 100, i + 2;
  return i + j;
}

function SimultaneousLets(): int {
  var i, v: bv32, b := 0, 0, true;
  var i, j := 100, i + 2;
  i + j
}

In lists of variable declarations, : binds stronger than ,

Simultaneous assignment (cont.)

method Swap<X>(a: array<X>, i: int, j: int) {
  a[i], a[j] := a[j], a[i];
}

method Example(a: array<int>, i: int, x: int) {
  if i != 3 || x == 5 {
    a[i], a[3] := 5, x;
  }
}

It is an error for a simultaneous assignment to give different values to the same l-value

While loop

method Zero(x: nat) returns (z: nat) {
  z := x;
  while z != 0 {
    z := z / 2;
  }
}

For loops

method InitUp(n: nat) returns (arr: array<int>) {
  arr := new int[n];
  for i := 0 to n {
    arr[i] := i;
  }
}
method InitDown(n: nat) returns (arr: array<int>) {
  arr := new int[n];
  for i := n downto 0 {
    arr[i] := i;
  }
}

• for i := lo to hi requires lo <= hi
• for i := hi downto lo requires lo <= hi
• The low bound is inclusive, the high bound exclusive
• for ... to post-increments the loop index
• for ... downto pre-decrements the loop index

For loops (cont.)

method Example() returns (arr: array<int>) {
  arr := new int[5];
  var m, n := 0, 5;
  for i := m to n {
    arr[i] := i;
    m, n := m - 123, n + 123;
  }
}

• for-loop bounds are determined on entry to the loop

If-case

method SadMax(x: int, y: int) returns (max: int) {
  if x < y {
    return x;
  } else {
    return y;
  }
}
method Max(x: int, y: int) returns (max: int) {
  if
  case x <= y =>
    return x;
  case y <= x =>
    return y;
}

Braces and scopes

method MoreThanMax(x: int, y: int) returns (m: int) {
  if {
    case x <= y =>
      var local := x + x;
      m := local - x;
    case y <= x =>
      m := y;
  }
  return m + 4;
}

• Variables declared in a case are local to that case
• Use braces if you follow the cases by a different statement
• Same for match statements and match expressions

While-case

method Gcd(x: nat, y: nat) returns (a: nat) {
  a := x;
  var b := y;
  while
  case a < b =>
    b := b - a;
  case b < a =>
    a := a - b;
}

Aggregate statement

method ArrayFill<X>(arr: array<X>, x: X) {
  forall i | 0 <= i < arr.Length {
    arr[i] := x;
  }
}
method Rotate<X>(arr: array<X>) {
  forall i | 0 <= i < arr.Length {
    arr[(i + 1) % arr.Length] := arr[i];
  }
}

• Note, a forall statement is an aggregate statement, not a loop
• Its body is performed simultaneously for all values of the bound variables
• Restrictions apply on the body (one assignment statement)

Choice

method Partition(arr: array<int>) {
  var pivot :| 1 <= pivot < arr.Length - 1;
  // ...
}

method Find(arr: array<int>, x: int) returns (i: int) {
  i :| 0 <= i < arr.Length && arr[i] == x;
}

There must exist a value for the bound variables

Binding guards

method MaybeFind(arr: array<int>, x: int) returns (r: nat) {
  if exists i :: 0 <= i < arr.Length && arr[i] == x {
    var i :| 0 <= i < arr.Length && arr[i] == x;
    return i;
  }
  return arr.Length;
}

method BindingIf(arr: array<int>, x: int) returns (r: nat) {
  if i :| 0 <= i < arr.Length && arr[i] == x {
    return i;
  }
  return arr.Length;
}

Modules and imports

module Library {
  method Sort(arr: array<int>)
}

module Client {
  import Library
  method Example() {
    var arr := new [] [10, 3, 8];
    Library.Sort(arr);
  }
}

Local names of imported modules

module Library {
  method Sort(arr: array<int>)
}

module Client {
  import L = Library
  method Example() {
    var arr := new [] [10, 3, 8];
    L.Sort(arr);
  }
}

Opened imports

module Library {
  newtype int32 = x | -0x8000_0000 <= x < 0x8000_0000
}

module Client {
  import opened Library
  function Difference(x: int32, y: int32): int32 {
    y - x
  }
}

Export set

module Library {
  export
    reveals Tree, Singleton
  datatype Tree = Leaf(int) | Node(Tree, Tree)
  function Singleton(x: int): Tree // ...
  function Combine(a: Tree, b: Tree): Tree // ...
}

module Client {
  import Library
  type DoubleTree = (Library.Tree, Library.Tree)
}

Export sets can be named

module Library {
  export Public
    reveals Tree, Singleton
  export Friends
    reveals Tree, Singleton, Combine

  // ...
}

module Client {
  import Library`Public
  type DoubleTree = (Library.Tree, Library.Tree)
}

Export extends

module Library {
  export Public
    reveals Tree, Singleton
  export Friends extends Public
    reveals Combine

  // ...
}

module Client {
  import Library`Public
  type DoubleTree = (Library.Tree, Library.Tree)
}

Eponymous export set

module Library {
  export
    reveals Tree, Singleton
  export Friends extends Library
    reveals Combine

  // ...
}

module Client {
  import Library
  type DoubleTree = (Library.Tree, Library.Tree)
}

Export provides

module Library {
  export
    reveals Tree, Singleton
    provides Combine

  datatype Tree = Leaf(int) | Node(Tree, Tree)
  function Singleton(x: int): Tree {
    Leaf(x)
  }
  function Combine(a: Tree, b: Tree): Tree {
    Node(a, b)
  }
}

Beyond compilation

A program is not just for the compiler

Ghost variables

method M(a: int, ghost b: int)
  returns (x: int, ghost y: int)
{
  ghost var u := a + b;
  u := u + 3;
  return 2 * a, 2 * u;
}

Ghost tuples

method M(a: int, ghost b: int)
  returns (x: int, ghost y: int)
{
  ghost var u := a + b;
  u := u + 3;
  return 2 * a, 2 * u;
}

function F(a: int, ghost b: int): (int, ghost int)
{
  ghost var u := a + b;
  ghost var u := u + 3;
  (2 * a, ghost 2 * u)
}

Auto-ghost

method M(a: int, ghost b: int)
  returns (x: int, ghost y: int)
{
  var u := a + b;
  u := u + 3;
  return 2 * a, 2 * u;
}

function F(a: int, ghost b: int): (int, ghost int)
{
  var u := a + b;
  var u := u + 3;
  (2 * a, ghost 2 * u)
}

Ghost fields, ghost methods

class Cell<X> {
  var data: X
  ghost var usageLog: seq<string>

  constructor (x: X) {
    usageLog := [];
    data := x;
    new;
    AppendToLog("creation");
  }

  ghost method AppendToLog(event: string) {
    usageLog := usageLog + [event];
  }
}

Ghost functions

datatype IncreasingList_ =
  | End(value: int)
  | Point(value: int, next: IncreasingList_)
{
  ghost predicate Valid() {
    Point? ==>
      && value <= next.value
      && next.Valid()
  }
}

type IncreasingList = ii: IncreasingList_ | ii.Valid()

Method specifications

newtype int32 = x: int | -0x8000_0000 <= x < 0x8000_0000

method Abs(x: int32) returns (r: int32)
  requires x != -0x8000_0000
  ensures 0 <= r
{
  if x < 0 {
    return -x;
  } else {
    return x;
  }
}

Function specifications

ghost predicate ContainsSymbols(expr: Expr) {
  || expr.Variable?
  || (expr.Plus? &&
      (ContainsSymbols(expr.0) || ContainsSymbols(expr.1)))
}
function Evaluate(expr: Expr): int
  requires !ContainsSymbols(expr)
{
  match expr
  case Const(value) => value
  case Plus(left, right) => Evaluate(left) + Evaluate(right)
}

So, Dafny has partial functions

Termination: recursion

function Sum(list: List<int>): int
  decreases list
{
  match list
  case Nil => 0
  case Cons(x, tail) => x + Sum(tail)
}

Termination: loops

method IterativeSum(list: List<int>) returns (s: int) {
  s := 0;
  var list := list;
  while list != Nil
    decreases list
  {
    s, list := s + list.head, list.tail;
  }
}

Loop invariants

method Combine(s: seq<int>) returns (r: int)
  ensures r % 2 == 0
{
  r := 0;
  for i := 0 to |s|
    invariant r % 2 == 0
  {
    var x := s[i];
    r := r + if x % 2 == 0 then x else x + x;
  }
}

Modifying state

method Increase(cell: Cell<int>)
  modifies cell
{
  cell.data := cell.data + 15;
}

Referring to previous state

method Increase(cell: Cell<int>)
  modifies cell
  ensures old(cell.data) < cell.data
{
  cell.data := cell.data + 15;
}