Logic in Dafny

based on Slides by Jean-Baptiste Tristan & K. Rustan M. Leino

Dafny as a proof assistant

Dafny is a genuine programming language
- Implemented using a compiler (including type checking) to write and execute programs
It is also a proof assistant
- You can state and prove mathematical propositions
- More generally, you can formalize mathematical theories
  - Arithmetic, set theory, group theory, measure theory, etc…
Our ultimate goal (and Dafny's purpose) is to verify programs, not mathematics
- Yet, an expert Dafny user must have a solid understanding of how to prove theorem in Dafny

Defining Algebraic Datatypes

  datatype Peano = 
    | Zero 
    | Succ(Peano)

What does Dafny know when we write this definition?

Algebraic Datatype Facts

  datatype Peano = 
    | Zero 
    | Succ(Peano)

The type Peano exists

Algebraic Datatype Facts

  datatype Peano = 
    | Zero 
    | Succ(Peano)

The type Peano exists (and is inhabited!)
Zero is constant element of the Peano datatype

Algebraic Datatype Facts

  datatype Peano = 
    | Zero 
    | Succ(Peano)

The type Peano exists
Zero is constant element of the Peano datatype
Given an element n of the Peano type, Succ(n) is also an element

Algebraic Datatype Facts

  datatype Peano = 
    | Zero 
    | Succ(Peano)

The type Peano exists
Zero is constant element of the Peano datatype
Given an element n of the Peano type, Succ(n) is also an element
Succ is injective
Succ and Zero are disjoint
Every element of Peano is formed by Succ or Zero
There is an induction principle!

Definition of theories

In Dafny, all of these can be expressed formally…

  type Peano(0) 

  ghost const Zero: Peano 

  ghost function Succ(n: Peano): Peano 

  lemma PeanoInjectivity(m: Peano, n: Peano)
    requires Succ(m) == Succ(n)
    ensures m == n

  lemma PeanoDiff(n: Peano)
    ensures Succ(n) != Zero 

  lemma PeanoExhaustive(n: Peano)
    ensures n == Zero || exists m: Peano :: n == Succ(m)

  lemma InductionPrinciple(P: Peano -> bool) 
    requires P(Zero) 
    requires forall n: Peano :: P(n) ==> P(Succ(n))
    ensures forall n: Peano :: P(n)

Theories

In Dafny, you define theories with
- Symbols
  - Types
  - Functions
  - Constants
  - Predicates
- Propositions

Type symbols

Dafny is a type theory:
- A proposition (mathematical statement) has a type: bool
- Any term that constitutes a proposition has a type
You can declare the existence of types and give them definitions
A type can be empty
Types can have type characteristics
- 00 says the type is nonempty
- Note that auto-init (0) implies nonempty (00)
NaturalNumber stands for a fixed but arbitrary, nonempty type
```
  type NaturalNumber(00)
```

Constant symbols

You can declare the existence of constants
They must have a type
```
  ghost const zero: NaturalNumber
```
zero stands for a fixed but arbitrary constant of type NaturalNumber
Since we are stating zero's existence, we need to know that NaturalNumber is nonempty
For now, think of the keyword ghost as telling us that this constant is a mathematical object, not a programming one

Function symbols

A constant with a function type is called a function

A function symbol can be declared by function

  ghost function Successor(n: NaturalNumber): NaturalNumber

Functions can have
- Type parameters
- Typed parameters
Functions have a return type

Predicate symbols

A function with return type bool is called a predicate

A predicate symbol can be declared by predicate

  ghost predicate Less(n: NaturalNumber, m: NaturalNumber)

Note that the “: bool” is implicit for a predicate

Lemmas

A functional (“executable”) expression of type bool represents a mathematical formula that can be false or true
They are sometimes called propositions

Propositions can be named using a lemma

  lemma Proposition()
    ensures forall m: int, n: int :: m > 0 && n > m ==> m + n > 0

A lemma has a name (here, Proposition)
The proposition stated by a lemma is given after the ensures keyword
- We call it the ensures clause of the lemma

Lemma schema

More generally, a lemma names a family of formulas

In the simplest case, the formula is unique

  lemma Prop() 
    ensures forall x: int :: x % 2 == 0 ==> (x / 2) * 2 == x

Schemas with parameters

The lemma can have type parameters and typed parameters
There is one formula for each possible instantiation of these parameters
```
  lemma Prop<T>(x: T) 
    ensures x == x
```

Schemas with preconditions

A lemma can have a requires clause, which is a precondition

It restricts the set of formulas to those whose parameterizations satisfy the precondition

  lemma Prop(x: int) 
    requires x % 2 == 0
    ensures (x / 2) * 2 == x

A General Schema

requires and ensures clauses contain propositions:

  lemma Prop(x1: T1,...) 
    requires proposition expression
    ensures proposition expression

Propositions != expressions

All functional expressions of type bool are valid propositions
Other RHS expressions are not valid propositions
Some propositions are not valid functional expressions

Propositional logic

Type: bool

  // Constants
  lemma False()
    ensures false 
  lemma True()
    ensures true 

  // Predicates
  lemma Conjunction(a: bool, b: bool)
    ensures a && b 
  lemma Disjunction(a: bool, b: bool)
    ensures a || b 
  lemma Implication(a: bool, b: bool)
    ensures a ==> b 
  lemma Explication(a: bool, b: bool)
    ensures a <== b 
  lemma Equivalence(a: bool, b: bool)
    ensures a <==> b 
  lemma Negation(a: bool)
    ensures !a

First-order logic

The language of propositions includes quantifiers that are not functional expressions

  type T
  
  ghost predicate P(x: T)

  lemma PredicateLogicConnectives()
    ensures (forall x: T :: P(x)) is bool
    ensures (exists x: T :: P(x)) is bool

Note: propositions need not be computable and they cannot always be compiled

Second-order logic

You can quantify over predicates and state properties from second order logic

  lemma SecondOrder()
    ensures forall P: int -> bool :: forall x: int :: P(x) || !P(x)

Higher-order logic

In fact, you can quantify over any value and Dafny is a higher-order logic

  lemma ThirdOrder()
    ensures forall P2: (int -> bool) -> bool :: forall P1: int -> bool :: P2(P1) || !P2(P1)

Impredicativity of propositions

Dafny is impredicative: a predicate can be defined by quantifying over all predicates

  lemma Impredicative()
    ensures forall x: T :: forall P: T -> bool :: P(x)

Predicativity of polymorphism

Dafny's polymorphism is predicative: type parameters always appear before typed parameters

Note, Dafny performs a syntactic rewrite called type-parameter completion on signatures¹

This ensures that all type arguments are filled in
This should not be confused for first-class higher-order type operators

  type List<X>

  function F<T>(x: T): T {
    x
  }

  function G(): List -> List {  // expands to:  function G<_T0>(): List<_T0> -> List<_T0>
    F<List>                     // expands to:  F<List<_T0>>
  }

Partiality

Dafny is a partial logic: some propositions, while syntactically correct, are rejected
In this example, Dafny rejects this proposition because 1/x is not defined for x == 0
```
  lemma Partial() 
    ensures forall x: int :: x * 1/x == x 
```
Note for experts:
- Dafny only pretends to be a partial logic
- In reality, it ensures that nothing can be proved about an undefined term
- The existing implementation requires propositions to be proved to be defined
- An implementation could also ensure that nothing can be proved about an undefined term

Partiality and proofs

Dafny therefore needs to verify whether a proposition is acceptable
To do so, it actually proves that the proposition is defined

In this example, Dafny can prove that x will not be equal to 0

  lemma Partial() 
    ensures forall x: int :: x != 0 ==> x / x == 1

Conclusion: in Dafny, the language of propositions depends on provability
And vice versa

Description

You can use Hilbert's Epsilon operator to choose a value satisfying some property

  predicate P(x: int)

  lemma HilbertEpsilon() 
    requires forall x: int :: P(x)
    ensures var x: int :| P(x); true

Referential transparency

Dafny is not referentially transparent²

The following proposition is false in Dafny:

  lemma NotReferentiallyTransparent()
    ensures (var x: int :| true; x) == (var x: int :| true; x)

Subtypes

You can combine a type and a proposition to define a subset type

  type T

  predicate P(x: T) 

  type U = x: T | P(x)
    witness *

Elements of type U are elements of type T that satisfy predicate P
A subset type is empty if the predicate never holds
The witness clause allows you to provide a witness if you want to guarantee that the type is inhabited
The witness * clause says that the type may be empty

Empty subset types

Example of nonempty subset type with a witness

  type T(00)

  ghost const k: T

  type U = x: T | true
    ghost witness k

Subtyping

If type U is defined as a subset type of T then U is a subtype of T

Consider the following types

  type T 

  predicate P1(x: T)

  type U = x: T | P1(x) witness *

  predicate P2(x: U)

  type V = x: U | P2(x) witness *

U is a subtype of T
- the inhabitants of U are those T inhabitants x for which P1(x) holds
V is a subtype of U
- the inhabitants of V are those U inhabitants x for which P2(x) holds
- the inhabitants of V are those T inhabitants x for which P1(x) && P2(x) holds

Subtyping for functions

Function type A -> B is a subtype of C -> D if

C is a subtype of A
B is a subtype of D

  lemma Subtyping(h: (V -> T) -> bool, f: U -> U)
    ensures h(f)

Covariant subtyping for type parameters

If a type operator S is covariant in its parameter (declared with +) then
- if U is a subtype of V, then S<U> is a subtype of S<V>
```
  type S<+X> 

  lemma Subtyping(f: S<U> -> bool, y: S<V>)
    ensures f(y) 
```

Contravariant subtyping for type parameters

If a type operator S is contravariant in its parameter (declared with -) then
- if U is a subtype of V, then S<V> is a subtype of S<U>
```
  type S<-X> 

  lemma Subtyping(f: S<U> -> bool, y: S<T>)
    ensures f(y)
```

Restrictions on type synonyms

To ensure that it remains consistent, Dafny sometimes rejects the definition of a type operator
```
  type S<!X> = X -> bool
```
In this example, because of how the type parameter X is used, Dafny asks for the parameter to be marked as !
This limits the how it can be instantiated
A covariant type parameter that needs to be restricted is declared as * instead of +

Axioms

The lemmas we have declared so far are (schemas of) axioms

By declaring the lemma we are making a statement that it is true

  lemma Axiom()
    ensures forall m: int, n: int :: m + n == n + m

Defining mathematical objects

When we axiomatize theories:
- We posit the existence of mathematicals objects such as types, constants, functions, and predicates
- We declare their properties
In general, declaring axioms must be avoided
- It is surprisingly easy to make a mistake leading to an inconsistent theory
Rather than assuming the existence of mathematical objects, it is better to define them

Defining constants

Rather than:

  ghost const x: int

  lemma EssenceOfX()
    ensures x == 0

A constant can be defined by assigning it an expression
```
  ghost const x: int := 0
```

Defining simple functions

Rather than:

  ghost function Increment(n: int): int

  lemma EssenceOfIncrement(n: int)
    ensures Increment(n) == n + 1

A function can be defined by providing it with a body

This body can be a functional expression

  ghost function Increment(n: int): int {
    n + 1
  }

Defining functions with quantifiers

The body of a mathematical function can also be a non-functional expression

  ghost predicate Valid(P: int -> bool) {
    forall x: int :: P(x)
  }

In general, a mathematical function may or may not be computable

Defining partial functions

Rather than:

  ghost function Divide(m: int, n: int): int

  lemma EssenceOfDivide(m: int, n: int)
    requires n != 0
    ensures Divide(m, n) == m / n

You can define a partial function

  ghost function Divide(m: int, n: int): int
    requires n != 0
  {
    m / n
  }

Defining functions by description

Hilbert's epsilon operator can be used to define functions

  predicate P<T>(m: T, n: T)

  ghost predicate Prop<T(!new)>(m: T) {
    exists n: T :: P(m, n)
  }

  ghost function F<T>(m: T): T
    requires Prop(m)
  {
    var n :| P(m, n);
    n
  }

You will rarely need this for routine program verification

Axiomatizing recursive functions

A function can be recursive

  ghost function Factorial(n: int): int

  lemma FactorialProp0()
    ensures Factorial(0) == 1

  lemma FactorialProp1(n: int)
    requires n > 0
    ensures Factorial(n) == n * Factorial(n - 1)

Danger of axiomatizing recursive functions

Axiomatizing recursive functions is error prone

  ghost function Factorial(n: int): int

  lemma FactorialBogus1(n: int)
    ensures Factorial(n) == n * Factorial(n - 1)

  lemma FactorialBogus2(n: int)
    ensures Factorial(n) == n * Factorial(n)

Defining recursive functions

Instead, the function can be defined

  ghost function Factorial(n: int): int 
    requires 0 <= n
  {
    if n == 0 then 1 else Factorial(n - 1)
  }

Existence of recursive functions

This raises an important question: how can Dafny ensure that this function actually exists?
One way is to make sure that the definition of the function is well-founded
Intuitively, it means that the function alwasy terminates
In the same way that Dafny tries to prove that propositions are defined automatically
- It also tries to prove that a function definition is well-founded on its own
- When it cannot, you need to help Dafny

Termination — easy case

In most cases, the termination metric is obvious and Dafny can infer it

  function Sum(n: int): int
    decreases n // this line can be omitted, because Dafny will infer it
  {
    if n <= 0 then 0 else Sum(n - 1)
  }

Termination — harder case

If not, you can give it a termination metric using a decreases clause

  function SumUpTo(counter: int, upTo: int): int
    decreases upTo - counter // here, the decreases clause is needed; Dafny will not infer it
  {
    if upTo <= counter then
      counter
    else
      counter + SumUpTo(counter + 1, upTo)
  }

The decrease clause is an expression that decreases at every recursive call

Definition of theories

When we axiomatize a theory, we posit the existence of types, constants, functions, …

  type Peano(0) 

  ghost const Zero: Peano 

  ghost function Succ(n: Peano): Peano 

  lemma PeanoInjectivity(m: Peano, n: Peano)
    requires Succ(m) == Succ(n)
    ensures m == n

  lemma PeanoDiff(n: Peano)
    ensures Succ(n) != Zero 

  lemma PeanoExhaustive(n: Peano)
    ensures n == Zero || exists m: Peano :: n == Succ(m)

  lemma InductionPrinciple(P: Peano -> bool) 
    requires P(Zero) 
    requires forall n: Peano :: P(n) ==> P(Succ(n))
    ensures forall n: Peano :: P(n)

ADT Definition

But you can just define algebraic datatypes to get the same theory
```
  datatype Peano = 
    | Zero 
    | Succ(Peano)
```