State of state in Dafny

State of state in Dafny

dafny-logo


K. Rustan M. Leino
Senior Principal Applied Scientist
Amazon Web Services

18 July 2023, Keynote, FTfJP 2023

What is Dafny?

  • Dafny started in 2008 as a

    programming language designed for verification

  • Today, Dafny's ecosystem includes

    • a verifier
    • 5+ compilers
    • IDE
    • unit test framework
    • documentation generator (a la Javadoc)
    • cross-language interaction (via Smithy-Dafny)
    • auditor

Virtues of Dafny

  • Write programs and prove them correct
  • Interface with multiple other languages
    • Dafny compiles to the runtime environments of
      C#, Java, JavaScript, Go, and Python
  • Write models and proofs
    • Interactive proof assistant
    • Higher-order logic (HOL) with partial functions and empty types

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)

book-cover

In progress

  • package manager
  • comprehensive standard library
  • additional language features
  • verification-performance analysis tools
  • …

Programming language

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

A few lessons

  • Stateful vs immutable data structures
  • Changing the rules
  • Dynamic-frames idiom

Mutable data structure

class List<X> {
  var value: X
  var next: List?<X>

  constructor (data: X) {
    value, next := data, null;
  }
}

Immutable data structure

datatype List<X> = Nil | Cons(head: X, tail: List<X>)

Class versus datatype

Use a class when

  • you need mutable fields, or
  • you think of each instance of a class as having its own identity

Otherwise, use a datatype

​

Many other modern languages support forms of both mutable and immutable data structures, but many encode one in terms of the other

Dafny changes the rules

Dafny offers

  • reference equality for classes, structural equality for datatypes
    • Look, Ma!  No .Equals methods!
  • functions
    • not pure methods
  • aggregate statements (forall)
    • which can replace many loops
  • tail recursion (modulo ghosts, and with auto accumulator)
    • instead of loops with remaining obligations
  • a fixed well-founded order for all types
    • instead of user-defined induction schemas

Reasoning about mutable data structures

  • Ownership
  • Permissions and separation logic
  • Dynamic frames

Demo

​

Extensible vector

Conclusions

  • Dafny is a powerful tool for formal reasoning
    • designed for writing programs
    • but also effective as interactive proof assistant
  • Dynamic frames are used to specify mutable data structures in the heap
    • but use immutable data structures when you can!
  • Look to change the rules
  • See also
    • dafny.org
    • program-proofs.com