REFERENCE
IMPLEMENTATION

of the decentralized

DAI STABLECOIN

issuance system

Nikolai Mushegian
Daniel Brockman
Mikael Brockman

[draft; 2018-02-06]

Contents

Introduction

The Dai stablecoin system is a set of blockchain smart contracts designed to issue a collateral-backed token (called the dai) and subject its price to a decentralized stability mechanism.

This document is an executable technical specification of the system. It is a draft and will change before launch.

For an overview of the system, see the white paper.

For a "choose your own adventure" exploration of the system's mechanics, please wait for the interactive FAQ.

We are dedicated to providing material for new people to understand the system in depth. This will be important for successful governance in the project's future.

If you have any questions, ask on our chat or subreddit. Asking helps us work on our explanatory material, so we appreciate it.

Why a reference implementation?

The contracts that will be deployed on the Ethereum blockchain are prototyped in Solidity. This paper is a model of the system written as a Haskell program. The motivations for this include:

Comparison. Checking two free-standing implementations against each other is a well-known way of ensuring that they both behave as intended.

Verification. Haskell lets us use powerful testing tools such as QuickCheck for comprehensively verifying key properties. This is a middle ground between testing and formal verification.

Formality. The work of translating into a purely functional program opens up opportunities for formal verification. This document will be useful for modelling aspects of the system in a proof assistant like Isabelle.

Explicitness. Coding the contract behavior in Haskell, a statically typed functional language, enforces explicit description of aspects which Solidity leaves implicit.

Clarity. An implementation not intended to be deployed on the blockchain is free from concerns about optimizing for gas cost and other factors that make the Solidity implementation less ideal as an understandable specification.

Simulation. Solidity is specific to the blockchain environment and lacks facilities for interfacing with files or other programs. A reference implementation is useful for doing simulations of the system's economic, game-theoretic, or statistical aspects.

Formal verification and steps thereto

We are developing automatic test suites that generate interaction sequences for property verification.

One such property is that the reference implementation behaves like the on-chain implementation. We verify this by generating Solidity test cases with equality assertions for the entire state.

Other key properties include

along with similar invariants and conditions. A future revision of this document will include formal statements of these properties.

Note on jargon

The reference implementation uses a concise vocabulary for system variables and actions.

This document has a glossary accessible through hovering over highlighted words.

Here are some of the motivations for this jargon:

Dai mechanics

The dai stablecoin system lets users lock collateral assets and issue dai in proportion to the collateral's market value. Thus they can deposit their valuable tokens in order to withdraw some quantity of stablecoin. Such a deposit account is called a "collateralized debt position" or CDP.

As long as such a deposit retains sufficient market value, the user may reclaim their deposit, partially or in whole, by paying back dai. As long as the CDP is collateralized in excess of the required ratio, the user can also decrease their collateralization by reclaiming part of the deposit without paying back dai.

Governance decides which external tokens are valid as collateral, and creates different deposit classes, or "CDP types", each with different parameters such as maximum dai issuance, minimum collateral ratio, and so on.

For deciding collateral requirements, the system values the dai not at the market price, but at its own target price, which is adjusted by the stability mechanism.

The target price adjustment is a second order effect. Primarily, the stability mechanism reacts to market price changes by adjusting the target rate.

Preamble and data types

This program uses some symbols defined in external libraries. Most symbols should be clear in context, but our "prelude" lists and briefly explains each imported type and function. Render the prelude.

module Maker where

import Prelude (); import Maker.Prelude; import Maker.Decimal

Numeric types

The system uses two precisions of decimal numbers, to which we have given short mnemonic names.

One is called wad and has 18 digits of precision. It is used for token quantities, such as amounts of ETH, DAI, or MKR.

The other is called ray and has 36 digits of precision. It is used for precise rates and ratios, such as the stability fee parameter.

We define these as distinct types. The type system will not allow us to combine them without explicit conversion.

newtype Wad = Wad (Decimal E18)
  deriving (Ord, Eq, Num, Real, Fractional, RealFrac)

newtype Ray = Ray (Decimal E36)
  deriving (Ord, Eq, Num, Real, Fractional, RealFrac)

We define a generic function for converting one of these types to the other.

cast x = fromRational (toRational x) -- [Via fractional $n/m$ form]

We also define a type for time durations in whole seconds.

newtype Sec = Sec Int
  deriving (Eq, Ord, Enum, Num, Real, Integral)

Identifiers and addresses

The following common Haskell idiom lets us use Id Ilk, Id Urn, and so on, as distinct identifier types.

newtype Id a = Id String
  deriving (Eq, Ord, Show)

We define another type for representing Ethereum account addresses.

newtype Address = Address String
  deriving (Eq, Ord, Show)

Gem, SIN, DAI, MKR: token identifiers

The system makes use of four basic types of tokens.

data Token

    -- Some collateral token approved by system governance
  = Gem (Id Tag)

    -- Fungible stablecoin, issued by CDP owners and traded publicly
  | DAI

    -- Internal anticoin whose quantity is always equal to total issued dai
  | SIN

    -- Volatile countercoin and voting token
  | MKR

  deriving (Eq, Ord, Show)

The system's approved collateral tokens are called "gems". We use the type Id Tag to denote the identity of some collateral token.

The model treats all collateral tokens as basic ERC20 tokens differing only in symbol. In reality, voters should make sure that tokens are well-behaved before approving them.

Tag: collateral token price record

The data received from price feeds is stored in Tag records.

data Tag = Tag {

  -- Latest token market price (denominated in SDR)
  _tag :: Wad,

  -- Timestamp after which price should be considered stale
  _zzz :: Sec

} deriving (Eq, Show)

Urn: CDP record

An Urn record keeps track of one CDP.

data Urn = Urn {

  -- CDP type identifier
  _ilk  :: Id Ilk,

  -- CDP owner
  _lad  :: Address,

  -- Amount of outstanding dai issued by this CDP, denominated in debt unit
  _art  :: Wad,

  -- Amount of collateral currently locked by this CDP
  _ink  :: Wad,

  -- Actor that triggered liquidation, if applicable
  _cat  :: Maybe Actor

} deriving (Eq, Show)

Ilk: CDP type record

An Ilk record keeps track of one CDP type.

data Ilk = Ilk {

  -- Token used as collateral for CDPs of this type
  _gem :: Id Tag,

  -- Total debt owed by CDPs of this type, denominated in debt unit
  _rum :: Wad,

  -- Current dai value of debt unit, increasing according to stability fee
  _chi :: Ray,

  -- Debt ceiling: maximum total outstanding dai value that can be issued by this CDP type
  _hat :: Wad,

  -- Liquidation ratio (collateral value per dai value)
  _mat :: Ray,

  -- Liquidation penalty (fraction of dai)
  _axe :: Ray,

  -- Fee (per-second fraction of dai)
  _tax :: Ray,

  -- Grace period of price feed unavailability
  _lax :: Sec,

  -- Timestamp of latest debt unit adjustment
  _rho :: Sec

} deriving (Eq, Show)

Vox: feedback mechanism record

The feedback mechanism is the aspect of the system that adjusts the target price of dai based on market price. Its data is grouped in a record called Vox.

data Vox = Vox {

  -- Dai market price denominated in SDR
  _wut :: Wad,

  -- Dai target price denominated in SDR
  _par :: Wad,

  -- Current per-second change in target price
  _way :: Ray,

  -- Sensitivity parameter (set by governance)
  _how :: Ray,

  -- Timestamp of latest feedback iteration
  _tau :: Sec

} deriving (Eq, Show)

Actor: account identifier

We use a data type to explicitly distinguish the different entities that can hold a token balance or invoke actions.

data Actor

    -- Extern address (CDP owner)
  = Account Address

    -- Collateral vault, holds all locked collateral until liquidation
  | Jar

    -- DAI and SIN are minted and burned by the "jug"
  | Jug

    -- The settler component
  | Vow

    -- The collateral auctioneer that raises DAI to cover liquidations
  | Flipper

    -- The "buy and burn" auctioneer that spends fee revenue on buying MKR
  | Flapper

    -- The "inflate and sell" auctioneer that mints MKR to cover liquidations
  | Flopper

    -- Test driver (not present in real system)
  | Toy

    -- Omnipotent actor (temporary kludge)
  | God

  deriving (Eq, Ord, Show)

System model

Finally we define the overall state of the model.

data System = System {

  -- Feedback mechanism data
  _vox      :: Vox,

  -- CDP records
  _urns     :: Map (Id Urn) Urn,

  -- CDP type records
  _ilks     :: Map (Id Ilk) Ilk,

  -- Price tags of collateral tokens
  _tags     :: Map (Id Tag) Tag,

  -- Token balances by actor and token
  _balances :: Map (Actor, Token) Wad,

  -- Current timestamp
  _era      :: Sec,

  -- Settler operation mode
  _mode     :: Mode,

  -- Sender of current action
  _sender   :: Actor,

  -- All user accounts (for tests)
  _accounts :: [Address]

} deriving (Eq, Show)
-- Settler-related work in progress
data Mode = Dummy
  deriving (Eq, Show)

Actions

The actions are the basic state transitions of the system.

Unless specified as internal, actions are accessible as public functions on the blockchain.

The auth modifier marks actions which can only be invoked from addresses to which the system has granted authority.

For details on the underlying »Action monad« which specifies how the action definitions behave with regard to state and rollback, see chapter \ref{chapter:monad}.

Issuance

Any user can open one or more accounts with the system using open, specifying a self-chosen account identifier and an ilk.

open id_urn id_ilk = do

 -- Fail if account identifier is taken
  none (urns . ix id_urn)

 -- Fail if ilk type is not present
  _ <- look (ilks . ix id_ilk)

 -- Create a CDP with the sender as owner
  Account id_lad <- use sender
  initialize (urns . at id_urn) (emptyUrn id_ilk id_lad)

The owner of an urn can transfer its ownership at any time using give.

give id_urn id_lad = do

 -- Fail if sender is not the CDP owner
  id_sender <- use sender
  owns id_urn id_sender

 -- Transfer CDP ownership
  assign (urns . ix id_urn . lad) id_lad

Unless CDP is in liquidation, its owner can use lock to lock more collateral.

lock id_urn wad_gem = do

 -- Fail if sender is not the CDP owner
  id_lad <- use sender
  owns id_urn id_lad

 -- Fail if liquidation in process
  want (feel id_urn) (not . oneOf [Grief, Dread])

 -- Identify collateral token
  id_ilk  <- look (urns . ix id_urn . ilk)
  id_tag  <- look (ilks . ix id_ilk . gem)

 -- Take custody of collateral
  transfer (Gem id_tag) wad_gem id_lad Jar

 -- Record an collateral token balance increase
  increase (urns . ix id_urn . ink) wad_gem

When a CDP has no risk problems (except that its ilk's ceiling may be exceeded), its owner can use free to reclaim some amount of collateral, as long as this would not take the CDP below its liquidation ratio.

free id_urn wad_gem = do

 -- Fail if sender is not the CDP owner
  id_lad <- use sender
  owns id_urn id_lad

 -- Record a collateral token balance decrease
  decrease (urns . ix id_urn . ink) wad_gem

 -- Roll back on any risk problem except ilk ceiling excess
  want (feel id_urn) (oneOf [Pride, Anger])

 -- Release custody of collateral
  id_ilk <- look (urns . ix id_urn . ilk)
  id_tag <- look (ilks . ix id_ilk . gem)
  transfer (Gem id_tag) wad_gem Jar id_lad

When a CDP has no risk problems, its owner can can use draw to issue fresh stablecoin, as long as the ilk ceiling is not exceeded and the issuance would not take the CDP below its liquidation ratio.

draw id_urn wad_dai = do

 -- Fail if sender is not the CDP owner
  id_lad <- use sender
  owns id_urn id_lad

 -- Update debt unit and unprocessed fee revenue
  id_ilk <- look (urns . ix id_urn . ilk)
  chi1 <- drip id_ilk

 -- Denominate issuance quantity in debt unit
  let wad_chi = wad_dai / cast chi1

 -- Record increase of CDP's stablecoin issuance
  increase (urns . ix id_urn . art) wad_chi

 -- Record increase of ilk's stablecoin issuance
  increase (ilks . ix id_ilk . rum) wad_chi

 -- Roll back on any risk problem
  want (feel id_urn) (== Pride)

 -- Mint both stablecoin and anticoin
  lend wad_dai

 -- Transfer stablecoin to CDP owner
  transfer DAI wad_dai Jug id_lad

An CDP owner who has previously issued stablecoin can use wipe to send back dai and reduce the CDP's issuance.

wipe id_urn wad_dai = do

 -- Fail if sender is not the CDP owner
  id_lad <- use sender
  owns id_urn id_lad

 -- Fail if CDP is in liquidation
  want (feel id_urn) (not . oneOf [Grief, Dread])

 -- Update debt unit and unprocessed fee revenue
  id_ilk <- look (urns . ix id_urn . ilk)
  chi1 <- drip id_ilk

 -- Denominate stablecoin amount in debt unit
  let wad_chi = wad_dai / cast chi1

 -- Record decrease of CDP issuance
  decrease (urns . ix id_urn . art) wad_chi

 -- Record decrease of ilk total issuance
  decrease (ilks . ix id_ilk . rum) wad_chi

 -- Take custody of stablecoin from CDP owner
  transfer DAI wad_dai id_lad Jar

 -- Destroy stablecoin and anticoin
  mend wad_dai

An CDP owner can use shut to close their account, if the price feed is up to date and the CDP is not in liquidation. This reclaims all collateral and cancels all issuance plus fee.

shut id_urn = do

 -- Update debt unit and unprocessed fee revenue
  id_ilk <- look (urns . ix id_urn . ilk)
  chi1 <- drip id_ilk

 -- Reverse all issued stablecoin plus fee
  art0 <- look (urns . ix id_urn . art)
  wipe id_urn (art0 * cast chi1)

 -- Reclaim all locked collateral
  ink0 <- look (urns . ix id_urn . ink)
  free id_urn ink0

 -- Nullify CDP record
  assign (urns . at id_urn) Nothing

Assessment

We define six stages of a CDP's lifecycle.

data Stage

    -- Overcollateralized, CDP type below debt ceiling, fresh price tag, liquidation not triggered
  = Pride

    -- Debt ceiling reached for CDP's type
  | Anger

    -- CDP type's collateral price feed in limbo
  | Worry

    -- CDP undercollateralized, or CDP type's price limbo grace period exceeded
  | Panic

    -- Liquidation triggered
  | Grief

    -- Liquidation triggered and started
  | Dread

  deriving (Eq, Show)

Lifecycle stage effects

The following table shows which CDP actions are allowed and prohibited in each stage of the CDP lifecycle.

decrease collateral ╭┈┈┈┈┈┈┈┈┈╮ give shut lock wipe free draw bite grab plop Pride ■ ■ ■ ■ ■ ■ Anger ■ ■ ■ ■ ■ Worry ■ ■ ■ ■ Panic ■ ■ ■ ■ ■ Grief ■ ■ Dread ■ ■ give shut lock wipe free draw bite grab plop ╰┈┈┈┈┈┈┈┈┈┈┈┈┈╯ ╰┈┈┈┈┈┈┈┈┈┈┈┈┈╯ increase collateral liquidation
Some implications:

CDP stage analysis

We define the function analyze that determines the lifecycle stage of a CDP.

analyze era0 par0 urn0 ilk0 tag0 =

  let

   -- Value of urn's locked collateral in SDR:
    pro = view ink urn0 * view tag tag0

   -- CDP's issuance denominated in SDR:
    con = view art urn0 * cast (view chi ilk0) * par0

   -- Required collateral value as per liquidation ratio:
    min = con * cast (view mat ilk0)

   -- CDP type's total DAI issuance:
    cap = view rum ilk0 * cast (view chi ilk0)

  in if

    -- Cases checked in order:
    | has cat urn0 && view ink urn0 == 0    -> Dread
    | has cat urn0                          -> Grief
    | pro < min                             -> Panic
    | view zzz tag0 + view lax ilk0 < era0  -> Panic
    | view zzz tag0 < era0                  -> Worry
    | cap > view hat ilk0                   -> Anger
    | otherwise                             -> Pride

Now we define the internal act feel which returns the value of analyze after ensuring that the system state is updated.

feel id_urn = do

 -- Adjust target price and target rate
  prod

 -- Update debt unit and unprocessed fee revenue
  id_ilk <- look (urns . ix id_urn . ilk)
  drip id_ilk

 -- Read parameters for stage analysis
  era0 <- use era
  par0 <- use (vox . par)
  urn0 <- look (urns . ix id_urn)
  ilk0 <- look (ilks . ix (view ilk urn0))
  tag0 <- look (tags . ix (view gem ilk0))

 -- Return lifecycle stage of CDP
  return (analyze era0 par0 urn0 ilk0 tag0)

CDP actions use feel to prohibit increasing risk when already risky, and to freeze stablecoin and collateral during liquidation.

Adjustment

The feedback mechanism is updated through prod, which can be invoked at any time by keepers, but is also invoked as a side effect of any CDP act that uses feel to assess risk.

prod = do

 -- Read all parameters relevant for feedback mechanism
  era0 <- use era
  tau0 <- use (vox . tau)
  wut0 <- use (vox . wut)
  par0 <- use (vox . par)
  how0 <- use (vox . how)
  way0 <- use (vox . way)

  let
   -- Time difference in seconds
    age  = era0 - tau0

   -- Current target rate applied to target price
    par1  = par0 * cast (way0 ^^ age)

   -- Sensitivity parameter applied over time
    wag  = how0 * fromIntegral age

   -- Target rate scaled up or down
    way1  = inj (prj way0 +
                 if wut0 < par0 then wag else -wag)

 -- Update target price
  assign (vox . par) par1

 -- Update rate of price change
  assign (vox . way) way1

 -- Record time of update
  assign (vox . tau) era0

  where
   -- Convert between multiplicative and additive form
    prj x  = if x >= 1  then x - 1  else 1 - 1 / x
    inj x  = if x >= 0  then x + 1  else 1 / (1 - x)

The stability fee of an ilk can change through governance. Due to the constraint that acts should run in constant time, the system cannot iterate over CDPs to effect such changes. Instead each ilk has a single »debt unit« which accumulates the stability fee. The drip act updates this unit. It can be called at any time by keepers, but is also called as a side effect of every act that uses feel to assess CDP risk.

drip id_ilk = do

  rho0  <- look (ilks . ix id_ilk . rho)
  tax0  <- look (ilks . ix id_ilk . tax)
  chi0  <- look (ilks . ix id_ilk . chi)
  rum0  <- look (ilks . ix id_ilk . rum)
  era0  <- use era

  let
   -- Time difference in seconds
    age   = era0 - rho0
   -- Value of debt unit increased according to stability fee
    chi1  = chi0 * tax0 ^^ age
   -- Stability fee revenue denominated in new unit
    dew   = (cast (chi1 - chi0) :: Wad) * rum0

 -- Mint stablecoin and anticoin for marginally accrued fee
  lend dew

 -- Record time of update
  assign (ilks . ix id_ilk . rho) era0

 -- Record new debt unit
  assign (ilks . ix id_ilk . chi) chi1

 -- Return the new debt unit
  return chi1

Price feed input

The mark act records a new market price of an collateral along with the expiration date of this price.

mark id_gem tag1 zzz1 = auth $ do
  initialize (tags . at id_gem) Tag {
    _tag  = tag1,
    _zzz  = zzz1
  }

The tell act records a new market price of dai along with the expiration date of this price.

tell wad = auth $ do
  assign (vox . wut) wad

Liquidation

When a CDP's stage marks it as in need of liquidation, any account can invoke the bite act to trigger the liquidation process. This enables the settler contract to grab the collateral for auctioning and take over the anticoin.

bite id_urn = do

 -- Fail if CDP is not in the appropriate stage
  want (feel id_urn) (== Panic)

 -- Record the sender as the liquidation initiator
  id_cat <- use sender
  assign (urns . ix id_urn . cat) (Just id_cat)

 -- Apply liquidation penalty to CDP issuance
  id_ilk <- look (urns . ix id_urn . ilk)
  axe0 <- look (ilks . ix id_ilk . axe)
  art0 <- look (urns . ix id_urn . art)
  let art1 = art0 * cast axe0

 -- Update CDP issuance to include penalty
  assign (urns . ix id_urn . art) art1

After liquidation has been triggered, the designated settler contract invokes grab to receive both the CDP's collateral and the anticoins corresponding to the CDP's issuance.

grab id_urn = auth $ do

 -- Fail if CDP is not marked for liquidation
  want (feel id_urn) (== Grief)

  ink0 <- look (urns . ix id_urn . ink)
  art0 <- look (urns . ix id_urn . art)
  id_ilk <- look (urns . ix id_urn . ilk)
  id_tag <- look (ilks . ix id_ilk . gem)

 -- Update the debt unit and unprocessed fee revenue
  chi1 <- drip id_ilk

 -- Denominate the issuance in dai
  let con = art0 * cast chi1

 -- Transfer collateral and anticoin to settler
  transfer (Gem id_tag) ink0 Jar Vow
  transfer SIN con Jug Vow

 -- Nullify CDP's collateral and anticoin quantities
  assign (urns . ix id_urn . ink) 0
  assign (urns . ix id_urn . art) 0

 -- Decrease the ilk's total issuance
  decrease (ilks . ix id_ilk . rum) art0

When the settler has finished the liquidation of a CDP, it invokes plop to give back any collateral it did not need to sell and restore the CDP.

plop id_urn wad_dai = auth $ do

 -- Fail unless CDP is in the proper stage
  want (feel id_urn) (== Dread)

 -- Forget the CDP's initiator of liquidation
  assign (urns . ix id_urn . cat) Nothing

 -- Take excess collateral from settler to vault
  id_vow <- use sender
  id_ilk <- look (urns . ix id_urn . ilk)
  id_tag <- look (ilks . ix id_ilk . gem)
  transfer (Gem id_tag) wad_dai id_vow Jar

 -- Record the excess collateral as belonging to the CDP
  assign (urns . ix id_urn . ink) wad_dai

The settler can invoke loot at any time to claim all uncollected stability fee revenue for use in the countercoin buy-and-burn auction.

loot = auth $ do

 -- The dai vault's balance is the uncollected stability fee revenue
  wad <- look (balance DAI Jug)

 -- Transfer the entire dai vault balance to sender
  transfer DAI wad Jug Vow

Auctioning

flip id_gem wad_jam wad_tab id_urn = do
  vow <- look mode
  case vow of
    Dummy -> return ()
flap = do
  vow <- look mode
  case vow of
    Dummy -> return ()

flop = do
  vow <- look mode
  case vow of
    Dummy -> return ()

Settlement

tidy who = auth $ do

 -- Find the entity's stablecoin and anticoin balances
  awe <- look (balance DAI who)
  woe <- look (balance SIN who)

 -- We can burn at most the smallest of the two balances
  let x = min awe woe

 -- Transfer stablecoin and anticoin to the settler
  transfer DAI x who Vow
  transfer SIN x who Vow

 -- Burn both stablecoin and anticoin
  burn DAI x Vow
  burn SIN x Vow
kick = do

 -- Transfer unprocessed stability fee revenue to vow account
  loot

 -- Cancel stablecoin against anticoin
  tidy Vow

 -- Assign any remaining stablecoin to countercoin-deflating auction
  transferAll DAI Vow Flapper
  flap

 -- Assign any remaining anticoin to countercoin-inflating auction
  transferAll SIN Vow Flopper
  flop

Governance

Governance uses form to create a new ilk. Since the new type is initialized with a zero ceiling, a separate transaction can safely set the risk parameters before any issuance occurs.

form id_ilk id_gem = auth $ do
  initialize (ilks . at id_ilk) (defaultIlk id_gem)

Governance uses frob to alter the sensitivity factor, which is the only mutable parameter of the feedback mechanism.

frob how1 = auth $ do
  assign (vox . how) how1

Governance can alter the five risk parameters of an ilk using cuff for the liquidation ratio; chop for the liquidation penalty; cork for the ilk ceiling; calm for the duration of price limbo; and crop for the stability fee.

cuff id_ilk mat1 = auth $ do
  assign (ilks . ix id_ilk . mat) mat1

chop id_ilk axe1 = auth $ do
  assign (ilks . ix id_ilk . axe) axe1

cork id_ilk hat1 = auth $ do
  assign (ilks . ix id_ilk . hat) hat1

calm id_ilk lax1 = auth $ do
  assign (ilks . ix id_ilk . lax) lax1

When altering the stability fee with crop, we ensure that the previous stability fee has been accounted for in the internal debt unit.

crop id_ilk tax1 = auth $ do

 -- Apply the current stability fee to the internal debt unit
  drip id_ilk

 -- Change the stability fee
  assign (ilks . ix id_ilk . tax) tax1

Token manipulation

We model the ERC20 transfer function in simplified form (omitting the concept of »allowance«).

transfer id_gem wad src dst =

 -- Operate in the token's balance table
  zoom balances $ do

 -- Fail if source balance insufficient
  balance <- look (ix (src, id_gem))
  aver (balance >= wad)

 -- Update balances
  decrease    (ix (src, id_gem)) wad
  initialize  (at (dst, id_gem)) 0
  increase    (ix (dst, id_gem)) wad
transferAll id_gem src dst = do
  wad <- look (balance id_gem src)
  transfer id_gem wad src dst

The internal act mint inflates the supply of a token. It is used by lend to create new stablecoin and anticoin, and by the settler to create new countercoin.

mint id_gem wad dst = do
  initialize (balances . at (dst, id_gem)) 0
  increase   (balances . ix (dst, id_gem)) wad

The internal act burn deflates the supply of a token. It is used by mend to destroy stablecoin and anticoin, and by the settler to destroy countercoin.

burn id_gem wad src =
  decrease (balances . ix (src, id_gem)) wad

The internal act lend mints identical amounts of both stablecoin and anticoin. It is used by draw to issue stablecoin; it is also used by drip to issue stablecoin representing revenue from stability fees, which stays in the vault until collected.

lend wad_dai = do
  mint DAI wad_dai Jug
  mint SIN wad_dai Jug

The internal act mend destroys identical amounts of both dai and the internal debt token. Its use via wipe is how the stablecoin supply is reduced.

mend wad_dai = do
  burn DAI wad_dai Jug
  burn SIN wad_dai Jug

Default data

defaultIlk :: Id Tag -> Ilk
defaultIlk id_tag = Ilk {
  _gem = id_tag,
  _axe = Ray 1,
  _mat = Ray 1,
  _tax = Ray 1,
  _hat = Wad 0,
  _lax = Sec 0,
  _chi = Ray 1,
  _rum = Wad 0,
  _rho = Sec 0
}
emptyUrn :: Id Ilk -> Address -> Urn
emptyUrn id_ilk id_lad = Urn {
  _cat = Nothing,
  _lad = id_lad,
  _ilk = id_ilk,
  _art = Wad 0,
  _ink = Wad 0
}
initialTag :: Tag
initialTag = Tag {
  _tag = Wad 0,
  _zzz = 0
}
initialSystem :: Ray -> System
initialSystem how0 = System {
  _balances = empty,
  _ilks     = empty,
  _urns     = empty,
  _tags     = empty,
  _era      = 0,
  _sender   = God,
  _accounts = mempty,
  _mode     = Dummy,
  _vox      = Vox {
    _tau = 0,
    _wut = Wad 1,
    _par = Wad 1,
    _how = how0,
    _way = Ray 1
  }
}

Action framework

The reader does not need any abstract understanding of monads to understand the code. They provide syntax (the do notation) for expressing exceptions and state in a way that is still purely functional. Each line of such a block is interpreted by the monad to provide the semantics we want.

The Action monad

This defines the Action monad as a simple composition of a state monad and an error monad:

type Action a = StateT System (Except Error) a

We divide act failure modes into general assertion failures and authentication failures.

data Error = AssertError Act | AuthError
  deriving (Show, Eq)

An act can be executed on a given initial system state using exec. The result is either an error or a new state. The exec function can also accept a sequence of actions, which will be interpreted as a single transaction.

exec :: System -> Action () -> Either Error System
exec sys m = runExcept (execStateT m sys)

Asserting

We now define a set of functions that fail unless some condition holds.

-- General assertion
aver x = unless x (throwError (AssertError ?act))

-- Assert that an indexed value is not present
none x = preuse x >>= \case
  Nothing -> return ()
  Just _  -> throwError (AssertError ?act)

-- Assert that an indexed value is present
look f = preuse f >>= \case
  Nothing -> throwError (AssertError ?act)
  Just x  -> return x

-- Execute an act and assert a condition on its result
want m p = m >>= (aver . p)

has p x = view p x /= Nothing

We define owns id_urn id_lad as an assertion that the given CDP is owned by the given account.

owns id_urn id_lad =
  want (look (urns . ix id_urn . lad)) ((== id_lad) . Account)

We define auth k as an act modifier that executes k only if the sender is authorized.

auth continue = do
  s <- use sender
  unless (s == God) (throwError AuthError)
  continue

Glossary

Id
Id a (for any a) is a string identifier that cannot be mixed up with some other Id b.
Urn
Urn is the data record for a CDP.
Ilk
Ilk is the data record for a CDP type.
lad
The lad of an Urn (type: Actor) is the account identifier of the owner of that CDP.
art
The art of an Urn (type: Wad) is the amount of outstanding dai issued by that CDP.
ink
The ink of an Urn (type: Wad) is the quantity of collateral locked in the corresponding CDP.
cat
The cat of an Urn is the actor which triggered the CDP's liquidation, if applicable.
gem
The gem of an Ilk is the collateral token used for collateral in the corresponding CDP type.
tax
The tax of an Ilk (type: Ray) is the stability fee imposed on CDPs of the corresponding CDP type, expressed as a per-second fraction of the CDP's outstanding dai.
lax
The lax of an Ilk (type: Sec) is the grace period for expired collateral price tags applying to CDPs of the corresponding type.
hat
The hat of an Ilk (type: Wad) is the maximum total ("ceiling") dai issuance for the corresponding CDP type.
rum
The rum of an Ilk (type: Wad) is the total current issuance for the corresponding CDP type, denominated in the CDP's internal debt unit.
chi
The chi of an Ilk (type: Ray) is the dai valuation for the corresponding CDP type's internal debt unit, compounding over time according to the CDP type's stability fee.
mat
The mat of an Ilk (type: Ray) is the minimum required collateralization ratio (value of collateral divided by value of issued dai) for CDPs of the corresponding CDP type.
axe
The axe of an Ilk (type: Ray) is the penalty imposed on liquidated CDPs of the corresponding CDP type, expressed as a fraction of the CDP's outstanding dai.
rho
The rho of an Ilk (type: Sec) is the timestamp of its latest debt unit adjustment.
tag
The tag of a Tag record (type: Wad) is the recorded market price of the corresponding collateral token denominated in SDR.
zzz
The zzz of a Tag (type: Sec) is the timestamp at which the corresponding collateral price tag will expire.
Pride
Pride is the risk stage of a non-risky CDP.
Anger
Anger is the Stage of a CDP whose type has reached its debt ceiling, but has a fresh price feed, is overcollateralized, and has not been triggered for liquidation.
Worry
Worry is the Stage of a CDP whose collateral price feed has expired yet is still within the CDP type's grace period; but the CDP is still considered overcollateralized and has not been triggered for liquidation. (The CDP's type may also have reached its debt ceiling.)
Panic
Panic is the Stage of a CDP which is undercollateralized or whose price feed is expired past the CDP type's grace period; but which has not yet been triggered for liquidation. (The CDP's type may also have reached its debt ceiling.)
Grief
Grief is the Stage of a CDP which has been triggered for liquidation.
Dread
Dread is the Stage of a CDP which is undergoing liquidation.
has
has k x is true if the field k of the record x is not Nothing.
Wad
Wad is the type of a decimal number with 18 decimals of precision, used for token quantities.
Ray
Ray is the type of a decimal number with 36 decimals of precision, used for precise rates and ratios.
Sec
Sec is the type of a timestamp or duration in whole seconds.
cast
cast x converts x to whatever numeric type is required in the expression context, possibly losing precision.
Address
Address represents an arbitrary Ethereum account address.
Token
Token identifies an ERC20 token used by the system: either some Gem (a collateral token) or one of SIN, DAI, or MKR.
Gem
Gem is a constructor for a Token representing a collateral token.
DAI
DAI is the identifier of the dai stablecoin token.
MKR
MKR is the identifier of the MKR token (the countercoin and governance token).
SIN
SIN is the identifier of the internal "anticoin" token which is always minted and burned in the same amounts as dai, only kept within the system as an accounting quantity.
wut
wut (type: Wad) is the feedback mechanism's latest market price of dai, denominated in SDR.
par
par (type: Wad) is the feedback mechanism's latest target price of dai, denominated in SDR.
way
way (type: Ray) is the current per-second change in target price, continuously altered by the feedback mechanism according to the sensitivity parameter.
how
how (type: Ray) is the sensitivity parameter of the feedback mechanism, set by governance, controlling the rate of change of the dai target price.
tau
tau (type: Sec) is the timestamp of the latest feedback mechanism iteration.
Tag
Tag is the record of collateral price feed updates. The type Id Tag is used to identify collateral tokens (aka Gems).
Vox
Vox is the record of feedback mechanism data.
Actor
Actor represents the identity of an entity which can hold a token balance or perform system actions.
Account
Account (type: Address -> Actor) constructs an Actor identifier denoting an external Ethereum account.
Jar
Jar (type: Actor) identifies the system's collateral vault.
Jug
Jug (type: Actor) identifies the actor that mints DAI/SIN and holds SIN.
Vow
Vow (type: Actor) identifies the system's settler component.
Flipper
Flipper (type: Actor) identifies the collateral auctioneer component.
Flapper
Flapper (type: Actor) identifies the DAI stablecoin auctioneer component.
Flopper
Flopper (type: Actor) identifies the MKR countercoin auctioneer component.
Toy
Toy (type: Actor) identifies the system's test driver (not present in production).
God
God (type: Actor) identifies an omnipotent actor (prototyping kludge, will be removed).
lock
lock transfers collateral from a CDP owner to the system's token vault and records an increase of ink to the CDP's Urn.
draw
draw mints new DAI for the owner of an overcollateralized CDP.
give
give transfers ownership of a CDP.
free
free reclaims collateral from an overcollateralized CDP.
prod
prod updates the stability feedback mechanism. It adjusts the target price (par) according to the target rate (way), and adjusts the target rate according to the current market price (wut) and the sensitivity parameter (how).
feel
feel calculates the Stage of a CDP. This involves deciding collateralization requirements as well as checking price feed status and liquidation progress.