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