Type-driven contract development

Jack Pettersson and Robert Edström
MSc thesis at Chalmers University of Technology, Sweden

Motivations

  • Catch bugs at compile time
  • What can be enforced using the type system?
  • Annotate types to generate boilerplate code
  • Functional paradigm

Case study:
Rock-paper-scissors

A game of two players. Joining costs exactly 10 ether.


contract RPS {
  uint nPlayers;
  mapping (address => move) public moves;
  function addPlayer(uint move) returns (boolean success) {
    if (nPlayers < 2 && msg.value >= 10) {
      moves[msg.sender] = move;
      nPlayers++;

      return true;
    else {

      return false;
    }
  }
  //[...]
}

Ether is not handled correctly!

Case study:
Rock-paper-scissors

Amended version


contract RPS {
  uint nPlayers;
  mapping (address => uint) public moves;
  function addPlayer(uint move) returns (boolean success) {
    if (nPlayers < 2 && msg.value >= 10) {
      moves[msg.sender] = move;
      nPlayers++;
      msg.sender.send(msg.value - 10);
      return true;
    else {
      msg.sender.send(msg.value);
      return false;
    }
  }
  //[...]
}

Better, but the move is still revealed!

Common errors

Mistake Solution
No handling of ether Encode ether flow in the type system
Openly communicating secret information Include crypto schemes in the language and stdlib

Catch errors using types

We start by including ether in the type signature: 


addPlayer : Int -> (success : Bool)
            { IN: value >= 10 }
  • Function is undefined for value < 10

Catch errors using types

Describe ether flow: 


addPlayer : Int -> (success : Bool)
            { IN:   value >= 10;
              SEND: success ? value - 10 : value;
              SAVE: success ? 10         : 0 }
  • saved+sent defined for all paths
  • Previous implementation wouldn't type check

Catch errors using types

Hide player move 


addPlayer : Commit Int -> (success : Bool)
            { IN:   value >= 10;
              SEND: success ? value - 10 : value;
              SAVE: success ? 10         : 0 }
  • Commitments part of the language
  • Revealing function is generated at compile-time
  • Accessed using a library function:
    
open : Commit a -> a

Type-correct implementation


addPlayer : Commit Int -> (success : Bool)
            { IN:   value >= 10;
              SEND: success ? value - 10 : value;
              SAVE: success ? 10         : 0 }
addPlayer {value} move = if !nPlayers < 2
                           then do save 10
                                   send (value-10) !sender
                                   // save move
                                   // increment counter
                                   return True
                           else do send value !sender
                                   return False

Implementation

Language: Idris

  • Very similar to Haskell, but...
  • Dependent types
  • Algebraic effects for environment interaction
  • Strictly evaluated

Summary

An expressive type-system can...

  • Catch large classes of errors at compile-time
  • Generate boiler-plate code
  • Provide compositionality

Work in progress

  • Lots of future work
  • Syntax and APIs in flux

THANK YOU

- https://github.com/vindaloo-thesis/examples

- Questions? Feedback? Ideas? Talk to us! :)

- jack.pettersson@consensys.net, robert@cacti.se