What follows is an executable K specification of the smart contracts of multicollateral dai.

Vat

The Vat stores the core dai, CDP, and collateral state, and tracks the system's accounting invariants. The Vat is where all dai is created and destroyed.

Specification of behaviours

Accessors

owners

The contracts use a multi-owner only-owner authorisation scheme. In the case of the Vat, all mutating methods can only be called by owners.

behaviour wards of Vat
interface wards(address guy)

storage
  // whether guy is an owner of Vat
  wards[guy] |-> Can

if
  VGas > 300000

returns Can

collateral type data

An ilk is a collateral type.

behaviour ilks of Vat
interface ilks(bytes32 ilk)

storage
  // collateral unit rate of ilk
  ilks[ilk].take |-> Take 
  // debt unit rate of ilk
  ilks[ilk].rate |-> Rate 
  // total locked collateral for ilk
  ilks[ilk].Ink  |-> Ink_i
  // total debt units issued from ilk
  ilks[ilk].Art  |-> Art_i

if
  VGas > 300000

returns Take : Rate : Ink_i : Art_i

urn data

An urn is a collateralised debt position.

behaviour urns of Vat
interface urns(bytes32 ilk, bytes32 urn)

storage
  // locked collateral units in ilk assigned to urn
  urns[ilk][urn].ink |-> Ink_iu
  // debt units in ilk assigned to urn
  urns[ilk][urn].art |-> Art_iu

if
  VGas > 300000

returns Ink_iu : Art_iu

internal unencumbered collateral balances

A gem is a token used as collateral in some ilk.

behaviour gem of Vat
interface gem(bytes32 ilk, bytes32 urn)

storage
  // unlocked collateral in ilk assigned to urn
  gem[ilk][urn] |-> Gem

if
  VGas > 300000

returns Gem

internal dai balances

dai is a stablecoin.

behaviour dai of Vat
interface dai(bytes32 lad)

storage
  // dai assigned to lad
  dai[lad] |-> Rad

if
  VGas > 300000

returns Rad

internal sin balances

sin, or "system debt", is used to track debt which is no longer assigned to a particular CDP, and is carried by the system during the liquidation process.

behaviour sin of Vat
interface sin(bytes32 lad)

storage
  // system debt assigned to lad
  sin[lad] |-> Rad

if
  VGas > 300000

returns Rad

total debt

behaviour debt of Vat
interface debt()

storage
  // total dai issued from the system
  debt |-> Debt

if
  VGas > 300000

returns Debt

total bad debt

behaviour vice of Vat
interface vice()

storage
  // total system debt
  vice |-> Vice

if
  VGas > 300000

returns Vice

Mutators

adding and removing owners

Any owner can add and remove owners.

behaviour deny of Vat
interface deny(address guy)

storage
  // whether CALLER_ID is an owner of Vat
  wards[CALLER_ID] |-> Can  
  // whether guy is an owner of Vat
  wards[guy]       |-> Could => 0

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

initialising an ilk

An ilk starts with Rate and Take set to (ray fixed-point) one.

behaviour init of Vat
interface init(bytes32 ilk)

storage
  // whether CALLER_ID is an owner of Vat
  wards[CALLER_ID] |-> Can 
  // debt unit rate of ilk
  ilks[ilk].rate   |-> Rate => 1000000000000000000000000000
  // collateral unit rate of ilk
  ilks[ilk].take   |-> Take => 1000000000000000000000000000

iff
  // caller is authorised
  Can == 1
  // Rate is zero
  Rate == 0
  // Take is zero
  Take == 0

if
  VGas > 300000

assigning unencumbered collateral

Collateral coming from outside of the system must be assigned to a user before it can be locked in a CDP.

behaviour slip of Vat
interface slip(bytes32 ilk, bytes32 guy, int256 wad)

storage
  // whether CALLER_ID is an owner of Vat
  wards[CALLER_ID] |-> Can
  // unlocked collateral in ilk assigned to guy
  gem[ilk][guy]    |-> Gem => Gem + wad

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

moving unencumbered collateral

behaviour flux of Vat
interface flux(bytes32 ilk, bytes32 src, bytes32 dst, int256 wad)

storage
  // whether CALLER_ID is an owner of Vat
  wards[CALLER_ID] |-> Can    
  // unlocked collateral in ilk assigned to src
  gem[ilk][src]    |-> Gem_src => Gem_src - wad
  // unlocked collateral in ilk assigned to dst
  gem[ilk][dst]    |-> Gem_dst => Gem_dst + wad

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

transferring dai balances

behaviour move of Vat
interface move(bytes32 src, bytes32 dst, int256 rad)

storage
  // whether CALLER_ID is an owner of Vat
  wards[CALLER_ID] |-> Can    
  // dai assigned to src
  dai[src]         |-> Dai_src => Dai_src - rad
  // dai assigned to dst
  dai[dst]         |-> Dai_dst => Dai_dst + rad

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

administering a position

This is the core method that opens, manages, and closes a collateralised debt position. This method has the ability to issue or delete dai while increasing or decreasing the position's debt, and to deposit and withdraw "encumbered" collateral from the position. The caller specifies the ilk i to interact with, and identifiers u, v, and w, corresponding to the sources of the debt, unencumbered collateral, and dai, respectively. The collateral and debt unit adjustments dink and dart are specified incrementally.

behaviour tune of Vat
interface tune(bytes32 i, bytes32 u, bytes32 v, bytes32 w, int256 dink, int256 dart)

storage
  // whether CALLER_ID is an owner of Vat
  wards[CALLER_ID] |-> Can   
  // collateral unit rate of i
  ilks[i].take     |-> Take  
  // debt unit rate of i
  ilks[i].rate     |-> Rate  
  // locked collateral units in i assigned to u
  urns[i][u].ink   |-> Ink_iu => Ink_iu + dink
  // debt units in i assigned to u
  urns[i][u].art   |-> Art_iu => Art_iu + dart
  // total locked collateral for i
  ilks[i].Ink      |-> Ink_i  => Ink_i  + dink
  // total debt units issued from i
  ilks[i].Art      |-> Art_i  => Art_i  + dart
  // unlocked collateral in i assigned to v
  gem[i][v]        |-> Gem_iv => Gem_iv - (Take * dink)
  // dai assigned to w
  dai[w]           |-> Dai_w  => Dai_w  + (Rate * dart)
  // total dai issued from the system
  debt             |-> Debt   => Debt   + (Rate * dart)

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

confiscating a position

When a position of a user u is siezed, both the collateral and debt are deleted from the user's account and assigned to the system's balance sheet, with the debt reincarnated as sin and assigned to some agent of the system w, while collateral goes to v.

behaviour grab of Vat
interface grab(bytes32 i, bytes32 u, bytes32 v, bytes32 w, int256 dink, int256 dart)

storage
  // whether CALLER_ID is an owner of Vat
  wards[CALLER_ID] |-> Can   
  // collateral unit rate of i
  ilks[i].take     |-> Take  
  // debt unit rate of i
  ilks[i].rate     |-> Rate  
  // locked collateral units in i assigned to u
  urns[i][u].ink   |-> Ink_iu => Ink_iu + dink
  // debt units in i assigned to u
  urns[i][u].art   |-> Art_iu => Art_iu + dart
  // total locked collateral for i
  ilks[i].Ink      |-> Ink_i  => Ink_i  + dink
  // total debt units issued from i
  ilks[i].Art      |-> Art_i  => Art_i  + dart
  // unlocked collateral in i assigned to v
  gem[i][v]        |-> Gem_iv => Gem_iv - (Take * dink)
  // system debt assigned to w
  sin[w]           |-> Sin_w  => Sin_w  - (Rate * dart)
  // total system debt
  vice             |-> Vice   => Vice   - (Rate * dart)

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

creating/annihilating system debt and surplus

dai and sin are two sides of the same coin. When the system has surplus dai, it can be cancelled with sin. Dually, the system can bring dai into existence while creating offsetting sin.

behaviour heal of Vat
interface heal(bytes32 u, bytes32 v, int256 rad)

storage
  // whether CALLER_ID is an owner of Vat
  wards[CALLER_ID] |-> Can  
  // dai assigned to v
  dai[v]           |-> Dai_v => Dai_v - rad
  // system debt assigned to u
  sin[u]           |-> Sin_u => Sin_u - rad
  // total dai issued from the system
  debt             |-> Debt  => Debt  - rad
  // total system debt
  vice             |-> Vice  => Vice  - rad

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

applying interest to an ilk

Interest is charged on an ilk i by adjusting the debt unit Rate, which says how many units of dai correspond to a unit of art. To preserve a key invariant, dai must be created or destroyed, depending on whether Rate is increasing or decreasing. The beneficiary/benefactor of the dai is u.

behaviour fold of Vat
interface fold(bytes32 i, bytes32 u, int256 rate)

storage
  // whether CALLER_ID is an owner of Vat
  wards[CALLER_ID] |-> Can  
  // debt unit rate of i
  ilks[i].rate     |-> Rate  => Rate + rate
  // total debt units issued from i
  ilks[i].Art      |-> Art_i
  // dai assigned to u
  dai[u]           |-> Dai   => Dai  + Art_i * rate
  // total dai issued from the system
  debt             |-> Debt  => Debt + Art_i * rate

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

applying collateral adjustment to an ilk

Likewise, the collateral unit Take can be adjusted, with collateral going to/from u.

behaviour toll of Vat
interface toll(bytes32 i, bytes32 u, int256 take)

storage
  // whether CALLER_ID is an owner of Vat
  wards[CALLER_ID] |-> Can 
  // collateral unit rate of i
  ilks[i].take     |-> Take => Take + take
  // total locked collateral for i
  ilks[i].Ink      |-> Ink 
  // unlocked collateral in i assigned to u
  gem[i][u]        |-> Gem  => Gem  - Ink * take

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

Drip

Specification of behaviours

Accessors

owners

behaviour wards of Drip
interface wards(address guy)

storage
  // whether guy is an owner of Drip
  wards[guy] |-> Can

if
  VGas > 300000

returns Can

ilk data

behaviour ilks of Drip
interface ilks(bytes32 ilk)

storage
  // stability fee of ilk
  ilks[ilk].tax |-> Tax
  // last drip time of ilk
  ilks[ilk].rho |-> Rho

if
  VGas > 300000

returns Tax : Rho

vat address

behaviour vat of Drip
interface vat()

storage
  // Vat that this Drip points to
  vat |-> Vat

if
  VGas > 300000

returns Vat

vow address

behaviour vow of Drip
interface vow()

storage
  // Vow that this Drip points to
  vow |-> Vow

if
  VGas > 300000

returns Vow

global interest rate

behaviour repo of Drip
interface repo()

storage
  // base interest rate
  repo |-> Repo

if
  VGas > 300000

returns Repo

getting the time

behaviour era of Drip
interface era()

if
  VGas > 300000

returns TIME

Mutators

adding and removing owners

behaviour deny of Drip
interface deny(address guy)

storage
  // whether CALLER_ID is an owner of Drip
  wards[CALLER_ID] |-> Can  
  // whether guy is an owner of Drip
  wards[guy]       |-> Could => 0

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

initialising an ilk

behaviour init of Drip
interface init(bytes32 ilk)

storage
  // whether CALLER_ID is an owner of Drip
  wards[CALLER_ID] |-> Can
  // stability fee of ilk
  ilks[ilk].tax    |-> Tax => #Ray
  // last drip time of ilk
  ilks[ilk].rho    |-> Rho => TIME

iff
  // caller is authorised
  Can == 1
  // Tax is zero
  Tax == 0

if
  VGas > 300000

setting ilk data

behaviour file of Drip
interface file(bytes32 ilk, bytes32 what, uint256 data)

storage
  // whether CALLER_ID is an owner of Drip
  wards[CALLER_ID] |-> Can
  // stability fee of ilk
  ilks[ilk].tax    |-> Tax => (#if what == #string2Word("tax") #then data #else Tax #fi)
  // last drip time of ilk
  ilks[ilk].rho    |-> Rho

iff
  // caller is authorised
  Can == 1
  // last drip was just now
  Rho == TIME

if
  VGas > 300000

setting the base rate

behaviour file-repo of Drip
interface file(bytes32 what, uint256 data)

storage
  // whether CALLER_ID is an owner of Drip
  wards[CALLER_ID] |-> Can 
  // base interest rate
  repo             |-> Repo => (#if what == #string2Word("repo") #then data #else Repo #fi)

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

setting the vow

behaviour file-vow of Drip
interface file(bytes32 what, bytes32 data)

storage
  // whether CALLER_ID is an owner of Drip
  wards[CALLER_ID] |-> Can
  // Vow that this Drip points to
  vow              |-> Vow => (#if what == #string2Word("vow") #then data #else Vow #fi)

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

updating the rates

behaviour drip of Drip
interface drip(bytes32 ilk)

storage
  // Vat that this Drip points to
  vat           |-> Vat 
  // Vow that this Drip points to
  vow           |-> Vow 
  // base interest rate
  repo          |-> Repo
  // stability fee of ilk
  ilks[ilk].tax |-> Tax 
  // last drip time of ilk
  ilks[ilk].rho |-> Rho  => TIME

storage Vat
  // whether ACCT_ID is an owner of Vat
  wards[ACCT_ID] |-> Can  
  // debt unit rate of ilk
  ilks[ilk].rate |-> Rate  => Rate + (#rmul(#rpow(Repo + Tax, TIME - Rho, #Ray), Rate) - Rate)
  // total debt units issued from ilk
  ilks[ilk].Art  |-> Art_i
  // dai assigned to Vow
  dai[Vow]       |-> Dai   => Dai  + Art_i * (#rmul(#rpow(Repo + Tax, TIME - Rho, #Ray), Rate) - Rate)
  // total dai issued from the system
  debt           |-> Debt  => Debt + Art_i * (#rmul(#rpow(Repo + Tax, TIME - Rho, #Ray), Rate) - Rate)

iff
  // caller is authorised
  Can == 1
  // call stack is not too big
  VCallDepth < 1024

if
  VGas > 300000

Pit

Specification of behaviours

Accessors

owners

behaviour wards of Pit
interface wards(address guy)

storage
  // whether guy is an owner of Pit
  wards[guy] |-> Can

if
  VGas > 300000

returns Can

ilk data

behaviour ilks of Pit
interface ilks(bytes32 ilk)

storage
  // collateral price in dai of ilk adjusted for liquidation ratio
  ilks[ilk].spot |-> Spot_i
  // debt ceiling for ilk
  ilks[ilk].line |-> Line_i

if
  VGas > 300000

returns Spot_i : Line_i

liveness

behaviour live of Pit
interface live()

storage
  // system liveness
  live |-> Live

if
  VGas > 300000

returns Live

vat address

behaviour vat of Pit
interface vat()

storage
  // Vat that this Pit points to
  vat |-> Vat

if
  VGas > 300000

returns Vat

global debt ceiling

behaviour Line of Pit
interface Line()

storage
  // global debt ceiling
  Line |-> Line

if
  VGas > 300000

returns Line

drip address

behaviour drip of Pit
interface drip()

storage
  // Drip that this Pit points to
  drip |-> Drip

if
  VGas > 300000

returns Drip

Mutators

adding and removing owners

behaviour deny of Pit
interface deny(address guy)

storage
  // whether CALLER_ID is an owner of Pit
  wards[CALLER_ID] |-> Can  
  // whether guy is an owner of Pit
  wards[guy]       |-> Could => 0

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

setting ilk data

behaviour file-ilk of Pit
interface file(bytes32 ilk, bytes32 what, uint256 data)

storage
  // whether CALLER_ID is an owner of Pit
  wards[CALLER_ID] |-> Can   
  // collateral price in dai of ilk adjusted for liquidation ratio
  ilks[ilk].spot   |-> Spot_i => #if what == #string2Word("spot") #then data #else Spot_i #fi
  // debt ceiling for ilk
  ilks[ilk].line   |-> Line_i => #if what == #string2Word("line") #then data #else Line_i #fi

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

setting the global debt ceiling

behaviour file-Line of Pit
interface file(bytes32 what, uint256 data)

storage
  // whether CALLER_ID is an owner of Pit
  wards[CALLER_ID] |-> Can 
  // global debt ceiling
  Line             |-> Line => #if what == #string2Word("Line") #then data #else Line #fi

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

manipulating a position

behaviour frob of Pit
interface frob(bytes32 ilk, int256 dink, int256 dart)

storage
  // system liveness
  live           |-> Live  
  // global debt ceiling
  Line           |-> Line  
  // Vat that this Pit points to
  vat            |-> Vat   
  // debt ceiling for ilk
  ilks[ilk].line |-> Line_i
  // collateral price in dai of ilk adjusted for liquidation ratio
  ilks[ilk].spot |-> Spot  

storage Vat
  // whether ACCT_ID is an owner of Vat
  wards[ACCT_ID]           |-> Can   
  // debt unit rate of ilk
  ilks[ilk].rate           |-> Rate  
  // collateral unit rate of ilk
  ilks[ilk].take           |-> Take  
  // total locked collateral for ilk
  ilks[ilk].Ink            |-> Ink_i  => Ink_i + dink
  // total debt units issued from ilk
  ilks[ilk].Art            |-> Art_i  => Art_i + dart
  // locked collateral units in ilk assigned to CALLER_ID
  urns[ilk][CALLER_ID].ink |-> Ink_iu => Ink_iu + dink
  // debt units in ilk assigned to CALLER_ID
  urns[ilk][CALLER_ID].art |-> Art_iu => Art_iu + dart
  // unlocked collateral in ilk assigned to CALLER_ID
  gem[ilk][CALLER_ID]      |-> Gem_u  => Gem_u - Take * dink
  // dai assigned to CALLER_ID
  dai[CALLER_ID]           |-> Dai    => Dai + Rate * dart
  // total dai issued from the system
  debt                     |-> Debt   => Debt + Rate * dart

iff
  // caller is authorised
  Can == 1
  // Rate is non-zero
  Rate =/= 0
  // position is either below collateral and global ceiling or is dai-decreasing
  (((((Art_iu + dart) * Rate) <= (#Ray * Spot)) and (((Debt + (Rate * dart))) < (#Ray * Line))) or (dart <= 0))
  // position is either safe or risk-decreasing
  (((dart <= 0) and (dink >= 0)) or (((Ink_iu + dink) * Spot) >= ((Art_iu + dart) * Rate)))
  // system is live
  Live == 1
  // call stack is not too big
  VCallDepth < 1024

if
  VGas > 300000

Vow

Specification of behaviours

Accessors

owners

behaviour wards of Vow
interface wards(address guy)

storage
  // whether guy is an owner of Vow
  wards[guy] |-> Can

if
  VGas > 300000

returns Can

getting the time

behaviour era of Vow
interface era()

if
  VGas > 300000

returns TIME

getting a sin packet

behaviour sin of Vow
interface sin(uint48 era)

storage
  // sin queued at timestamp era
  sin[era] |-> Sin_era

if
  VGas > 300000

returns Sin_era

getting the Sin

behaviour Sin of Vow
interface Sin()

storage
  // total queued sin
  Sin |-> Sin

if
  VGas > 300000

returns Sin

getting the Woe

behaviour Woe of Vow
interface Woe()

storage
  // total matured sin
  Woe |-> Woe

if
  VGas > 300000

returns Woe

getting the Ash

behaviour Ash of Vow
interface Ash()

storage
  // total sin in debt auctions
  Ash |-> Ash

if
  VGas > 300000

returns Ash

getting the wait

behaviour wait of Vow
interface wait()

storage
  // sin maturation time
  wait |-> Wait

if
  VGas > 300000

returns Wait

getting the sump

behaviour sump of Vow
interface sump()

storage
  // debt auction lot size
  sump |-> Sump

if
  VGas > 300000

returns Sump

getting the bump

behaviour bump of Vow
interface bump()

storage
  // surplus auction lot size
  bump |-> Bump

if
  VGas > 300000

returns Bump

getting the hump

behaviour hump of Vow
interface hump()

storage
  // surplus dai cushion
  hump |-> Hump

if
  VGas > 300000

returns Hump

getting the Awe

behaviour Awe of Vow
interface Awe()

storage
  // total queued sin
  Sin |-> Sin
  // total matured sin
  Woe |-> Woe
  // total sin in debt auctions
  Ash |-> Ash

if
  VGas > 300000

returns Sin + Woe + Ash

getting the Joy

behaviour Joy of Vow
interface Joy()

storage
  // Vat that this Vow points to
  vat |-> Vat

storage Vat
  // dai assigned to ACCT_ID
  dai[ACCT_ID] |-> Dai

iff
  // call stack is not too big
  VCallDepth < 1024

if
  VGas > 300000

returns Dai / #Ray

Mutators

adding and removing owners

behaviour deny of Vow
interface deny(address guy)

storage
  // whether CALLER_ID is an owner of Vow
  wards[CALLER_ID] |-> Can  
  // whether guy is an owner of Vow
  wards[guy]       |-> Could => 0

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

setting Vow parameters

behaviour file-data of Vow
interface file(bytes32 what, uint256 data)

storage
  // whether CALLER_ID is an owner of Vow
  wards[CALLER_ID] |-> Can 
  // sin maturation time
  wait             |-> Wait => (#if what == #string2Word("wait") #then data #else Wait #fi)
  // debt auction lot size
  sump             |-> Sump => (#if what == #string2Word("sump") #then data #else Sump #fi)
  // surplus auction lot size
  bump             |-> Bump => (#if what == #string2Word("bump") #then data #else Bump #fi)
  // surplus dai cushion
  hump             |-> Hump => (#if what == #string2Word("hump") #then data #else Hump #fi)

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

setting vat and liquidators

behaviour file-addr of Vow
interface file(bytes32 what, address addr)

storage
  // whether CALLER_ID is an owner of Vow
  wards[CALLER_ID] |-> Can
  // Flapper that this Vow points to
  cow              |-> Cow => (#if what == #string2Word("flap") #then addr #else Cow #fi)
  // Flopper that this Vow points to
  row              |-> Row => (#if what == #string2Word("flop") #then addr #else Row #fi)
  // Vat that this Vow points to
  vat              |-> Vat => (#if what == #string2Word("vat")  #then addr #else Vat #fi)

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

cancelling bad debt and surplus

behaviour kiss of Vow
interface kiss(uint256 wad)

storage
  // Vat that this Vow points to
  vat |-> Vat
  // total sin in debt auctions
  Ash |-> Ash => Ash - wad

storage Vat
  // whether ACCT_ID is an owner of Vat
  wards[ACCT_ID] |-> Can 
  // dai assigned to ACCT_ID
  dai[ACCT_ID]   |-> Dai  => Dai  - wad * #Ray
  // system debt assigned to ACCT_ID
  sin[ACCT_ID]   |-> Sin  => Sin  - wad * #Ray
  // total system debt
  vice           |-> Vice => Vice - wad * #Ray
  // total dai issued from the system
  debt           |-> Debt => Debt - wad * #Ray

iff
  // caller is authorised
  Can == 1
  // call stack is not too big
  VCallDepth < 1024

if
  VGas > 300000

adding to the sin queue

behaviour fess of Vow
interface fess(uint256 tab)

storage
  // whether CALLER_ID is an owner of Vow
  wards[CALLER_ID] |-> Can    
  // sin queued at timestamp TIME
  sin[TIME]        |-> Sin_era => Sin_era + tab
  // total queued sin
  Sin              |-> Sin     => Sin     + tab

iff
  // caller is authorised
  Can == 1
  // call stack is not too big
  VCallDepth < 1024

if
  VGas > 300000

processing sin queue

behaviour flog of Vow
interface flog(uint48 t)

storage
  // sin maturation time
  wait   |-> Wait 
  // total queued sin
  Sin    |-> Sin   => Sin - Sin_t
  // total matured sin
  Woe    |-> Woe   => Woe + Sin_t
  // sin queued at timestamp t
  sin[t] |-> Sin_t => 0

iff
  // sin has matured
  t + Wait <= TIME
  // call stack is not too big
  VCallDepth < 1024

if
  VGas > 300000

starting a debt auction

behaviour flop of Vow
interface flop()

storage
  // Flopper that this Vow points to
  row  |-> Row 
  // Vat that this Vow points to
  vat  |-> Vat 
  // debt auction lot size
  sump |-> Sump
  // total matured sin
  Woe  |-> Woe  => Woe - Sump
  // total sin in debt auctions
  Ash  |-> Ash  => Ash + Sump

storage Row
  // whether ACCT_ID is an owner of Flop
  #Flop.wards[ACCT_ID]              |-> Can                                                 
  // auction counter
  #Flop.kicks                       |-> Kicks                                                => 1 + Kicks
  // beneficiary of the auction
  #Flop.bids[1 + Kicks].vow         |-> Vow_was                                              => ACCT_ID
  // current bid (dai)
  #Flop.bids[1 + Kicks].bid         |-> Bid_was                                              => Sump
  // current lot (gem)
  #Flop.bids[1 + Kicks].lot         |-> Lot_was                                              => maxUInt256
  // 
  #Flop.bids[1 + Kicks].guy_tic_end |-> #WordPackAddrUInt48UInt48(Guy_was, Tic_was, End_was) => #WordPackAddrUInt48UInt48(ACCT_ID, Tic_was, TIME + Tau)
  // 
  #Flop.ttl_tau                     |-> #WordPackUInt48UInt48(Ttl, Tau)                     

storage Vat
  // dai assigned to ACCT_ID
  dai[ACCT_ID] |-> Dai

iff
  // caller is authorised
  Can == 1
  // there is at most dust Joy
  Dai < #Ray
  // call stack is not too big
  VCallDepth < 1024

if
  VGas > 300000

returns 1 + Kicks

starting a surplus auction

behaviour flap of Vow
interface flap()

storage
  // Flapper that this Vow points to
  cow  |-> Cow 
  // Vat that this Vow points to
  vat  |-> Vat 
  // surplus auction lot size
  bump |-> Bump
  // surplus dai cushion
  hump |-> Hump
  // total queued sin
  Sin  |-> Sin 
  // total matured sin
  Woe  |-> Woe 
  // total sin in debt auctions
  Ash  |-> Ash 

storage DaiMove
  // Vat that this DaiMove points to
  vat               |-> Vat
  // Cow is authorised to move for ACCT_ID
  can[ACCT_ID][Cow] |-> Can => Can

storage Cow
  // dai token
  #Flap.dai                         |-> DaiMove                                             
  // 
  #Flap.ttl_tau                     |-> #WordPackUInt48UInt48(Ttl, Tau)                     
  // auction counter
  #Flap.kicks                       |-> Kicks                                                => 1 + Kicks
  // current bid (dai)
  #Flap.bids[1 + Kicks].bid         |-> Bid_was                                              => 0
  // current lot (gem)
  #Flap.bids[1 + Kicks].lot         |-> Lot_was                                              => Bump
  // 
  #Flap.bids[1 + Kicks].guy_tic_end |-> #WordPackAddrUInt48UInt48(Guy_was, Tic_was, End_was) => #WordPackAddrUInt48UInt48(ACCT_ID, Tic_was, TIME + Tau)
  // beneficiary of the auction
  #Flap.bids[1 + Kicks].gal         |-> Gal_was                                              => ACCT_ID

storage Vat
  // whether DaiMove is an owner of Vat
  wards[DaiMove] |-> Can_move
  // dai assigned to ACCT_ID
  dai[ACCT_ID]   |-> Dai      => Dai - #Ray * Bump

iff
  // there is enough Joy
  Dai / #Ray >= (((Sin + Woe) + Ash) + Bump) + Hump
  // there is no Woe
  Woe == 0
  // call stack is not too big
  VCallDepth < 1022

if
  Cow =/= DaiMove
  Cow =/= Vat
  Vat =/= DaiMove
  VGas > 300000

returns 1 + Kicks

Cat

Specification of behaviours

Accessors

owners

behaviour wards of Cat
interface wards(address guy)

storage
  // whether guy is an owner of Cat
  wards[guy] |-> Can

if
  VGas > 300000

returns Can

ilk data

behaviour ilks of Cat
interface ilks(bytes32 ilk)

storage
  // Flipper for ilk
  ilks[ilk].flip |-> Flip
  // liquidation penalty for ilk
  ilks[ilk].chop |-> Chop
  // liquidation lot size for ilk
  ilks[ilk].lump |-> Lump

if
  VGas > 300000

returns Flip : Chop : Lump

liquidation data

behaviour flips of Cat
interface flips(uint256 n)

storage
  // collateral type for flip n
  flips[n].ilk |-> Ilk
  // owner identifier for flip n
  flips[n].urn |-> Urn
  // collateral in flip n
  flips[n].ink |-> Ink
  // debt in flip n
  flips[n].tab |-> Tab

if
  VGas > 300000

returns Ilk : Urn : Ink : Tab

liquidation counter

behaviour nflip of Cat
interface nflip()

storage
  // flip count
  nflip |-> Nflip

if
  VGas > 300000

returns Nflip

liveness

behaviour live of Cat
interface live()

storage
  // system liveness
  live |-> Live

if
  VGas > 300000

returns Live

vat address

behaviour vat of Cat
interface vat()

storage
  // Vat that this Cat points to
  vat |-> Vat

if
  VGas > 300000

returns Vat

pit address

behaviour pit of Cat
interface pit()

storage
  // Pit that this Cat points to
  pit |-> Pit

if
  VGas > 300000

returns Pit

vow address

behaviour vow of Cat
interface vow()

storage
  // Vow that this Cat points to
  vow |-> Vow

if
  VGas > 300000

returns Vow

Mutators

addingg and removing owners

behaviour deny of Cat
interface deny(address guy)

storage
  // whether CALLER_ID is an owner of Cat
  wards[CALLER_ID] |-> Can  
  // whether guy is an owner of Cat
  wards[guy]       |-> Could => 0

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

setting contract addresses

behaviour file-addr of Cat
interface file(bytes32 what, address data)

storage
  // whether CALLER_ID is an owner of Cat
  wards[CALLER_ID] |-> Can
  // Pit that this Cat points to
  pit              |-> Pit => (#if what == #string2Word("pit") #then data #else Pit #fi)
  // Vow that this Cat points to
  vow              |-> Vow => (#if what == #string2Word("vow") #then data #else Vow #fi)

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

setting liquidation data

behaviour file of Cat
interface file(bytes32 ilk, bytes32 what, uint256 data)

storage
  // whether CALLER_ID is an owner of Cat
  wards[CALLER_ID] |-> Can 
  // liquidation penalty for ilk
  ilks[ilk].chop   |-> Chop => (#if what == #string2Word("chop") #then data #else Chop #fi)
  // liquidation lot size for ilk
  ilks[ilk].lump   |-> Lump => (#if what == #string2Word("lump") #then data #else Lump #fi)

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

setting liquidator address

behaviour file-flip of Cat
interface file(bytes32 ilk, bytes32 what, address data)

storage
  // whether CALLER_ID is an owner of Cat
  wards[CALLER_ID] |-> Can 
  // Flipper for ilk
  ilks[ilk].flip   |-> Flip => (#if what == #string2Word("flip") #then data #else Flip #fi)

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

marking a position for liquidation

behaviour bite of Cat
interface bite(bytes32 ilk, address urn)

storage
  // Vat that this Cat points to
  vat              |-> Vat    
  // Pit that this Cat points to
  pit              |-> Pit    
  // Vow that this Cat points to
  vow              |-> Vow    
  // flip count
  nflip            |-> Nflip   => Nflip + 1
  // collateral type for flip Nflip
  flips[Nflip].ilk |-> Ilk_was => ilk
  // owner identifier for flip Nflip
  flips[Nflip].urn |-> Urn_was => urn
  // collateral in flip Nflip
  flips[Nflip].ink |-> Ink_was => Ink_iu
  // debt in flip Nflip
  flips[Nflip].tab |-> Tab_was => Rate * Art_iu
  // system liveness
  live             |-> Live   

storage Vat
  // whether ACCT_ID is an owner of Vat
  wards[ACCT_ID]     |-> Can   
  // collateral unit rate of ilk
  ilks[ilk].take     |-> Take  
  // debt unit rate of ilk
  ilks[ilk].rate     |-> Rate  
  // locked collateral units in ilk assigned to urn
  urns[ilk][urn].ink |-> Ink_iu => 0
  // debt units in ilk assigned to urn
  urns[ilk][urn].art |-> Art_iu => 0
  // total locked collateral for ilk
  ilks[ilk].Ink      |-> Ink_i  => Ink_i  - Ink_iu
  // total debt units issued from ilk
  ilks[ilk].Art      |-> Art_i  => Art_i  - Art_iu
  // unlocked collateral in ilk assigned to ACCT_ID
  gem[ilk][ACCT_ID]  |-> Gem_iv => Gem_iv + Take * Ink_iu
  // system debt assigned to Vow
  sin[Vow]           |-> Sin_w  => Sin_w  - Rate * Art_iu
  // total system debt
  vice               |-> Vice   => Vice   - Rate_* Art_iu

storage Pit
  // collateral price in dai of ilk adjusted for liquidation ratio
  ilks[ilk].spot |-> Spot_i

storage Vow
  // sin queued at timestamp TIME
  sin[TIME] |-> Sin_era => Sin_era + Art_iu * Rate
  // total queued sin
  Sin       |-> Sin     => Sin     + Art_iu * Rate

iff
  // caller is authorised
  Can == 1
  // system is live
  Live == 1
  // CDP is vulnerable
  Ink_iu * Spot_i < Art_iu * Rate
  // call stack is not too big
  VCallDepth < 1024

if
  VGas > 300000

returns Nflip + 1

starting a collateral auction

behaviour flip of Cat
interface flip(uint256 n, uint256 wad)

storage
  // collateral type for flip n
  flips[n].ilk   |-> Ilk 
  // owner identifier for flip n
  flips[n].urn   |-> Urn 
  // collateral in flip n
  flips[n].ink   |-> Ink  => Ink - (Ink * wad) / Tab
  // debt in flip n
  flips[n].tab   |-> Tab  => Tab - wad
  // Flipper for ilk
  ilks[ilk].flip |-> Flip
  // liquidation penalty for ilk
  ilks[ilk].chop |-> Chop
  // liquidation lot size for ilk
  ilks[ilk].lump |-> Lump
  // Vow that this Cat points to
  vow            |-> Vow 
  // system liveness
  live           |-> Live

storage Flip
  // 
  ttl_tau                     |-> #WordPackUInt48UInt48(Ttl, Tau)
  // auction counter
  kicks                       |-> Kicks                           => 1 + Kicks
  // current bid (dai)
  bids[1 + Kicks].bid         |-> _                               => 0
  // current lot (gem)
  bids[1 + Kicks].lot         |-> _                               => (Ink * wad) / Tab
  // 
  bids[1 + Kicks].guy_tic_end |-> _                               => #WordPackAddrUInt48UInt48(ACCT_ID, 0, TIME + Tau)
  // beneficiary of remaining gems
  bids[1 + Kicks].urn         |-> _                               => Urn
  // beneficiary of dai
  bids[1 + Kicks].gal         |-> _                               => Vow
  // debt to cover
  bids[1 + Kicks].tab         |-> _                               => (wad * Chop) /Int 1000000000000000000000000000)

iff
  // system is live
  Live == 1
  // flipping no more than the available debt
  wad <= Tab
  // flipping the lot size or the remainder
  (wad == Lump) or ((wad < Lump) and (wad == Tab))
  // call stack is not too big
  VCallDepth < 1023

if
  VGas > 300000

returns 1 + Kicks

GemJoin

Specification of behaviours

Accessors

vat address

behaviour vat of GemJoin
interface vat()

storage
  // Vat that this adapter points to
  vat |-> Vat

if
  VGas > 300000

returns Vat

the associated ilk

behaviour ilk of GemJoin
interface ilk()

storage
  // collateral type of this adapter
  ilk |-> Ilk

if
  VGas > 300000

returns Ilk

gem address

behaviour gem of GemJoin
interface gem()

storage
  // underlying token of this adapter
  gem |-> Gem

if
  VGas > 300000

returns Gem

Mutators

depositing into the system

behaviour join of GemJoin
interface join(bytes32 urn, uint256 wad)

storage
  // Vat that this adapter points to
  vat |-> Vat
  // collateral type of this adapter
  ilk |-> Ilk
  // underlying token of this adapter
  gem |-> Gem

storage Vat
  // whether ACCT_ID is an owner of Vat
  wards[ACCT_ID]      |-> Can
  // unlocked collateral in Ilk assigned to CALLER_ID
  gem[Ilk][CALLER_ID] |-> Rad => Rad + #Ray * wad

storage Gem
  // gem balance of CALLER_ID
  balances[CALLER_ID] |-> Bal_guy     => Bal_guy     - wad
  // gem balance of ACCT_ID
  balances[ACCT_ID]   |-> Bal_adapter => Bal_adapter + wad

iff
  // caller is authorised
  Can == 1
  // call stack is not too big
  VCallDepth < 1024

if
  VGas > 300000

withdrawing from the system

behaviour exit of GemJoin
interface exit(address guy, uint256 wad)

storage
  // Vat that this adapter points to
  vat |-> Vat
  // collateral type of this adapter
  ilk |-> Ilk
  // underlying token of this adapter
  gem |-> Gem

storage Vat
  // whether ACCT_ID is an owner of Vat
  wards[ACCT_ID]      |-> Can
  // unlocked collateral in Ilk assigned to CALLER_ID
  gem[Ilk][CALLER_ID] |-> Rad => Rad - #Ray * wad

storage Gem
  // gem balance of CALLER_ID
  balances[CALLER_ID] |-> Bal_guy     => Bal_guy     + wad
  // gem balance of ACCT_ID
  balances[ACCT_ID]   |-> Bal_adapter => Bal_adapter - wad

iff
  // caller is authorised
  Can == 1
  // call stack is not too big
  VCallDepth < 1024

if
  VGas > 300000

ETHJoin

Specification of behaviours

Accessors

vat address

behaviour vat of ETHJoin
interface vat()

storage
  // Vat that this adapter points to
  vat |-> Vat

if
  VGas > 300000

returns Vat

the associated ilk

behaviour ilk of ETHJoin
interface ilk()

storage
  // collateral type of this adapter
  ilk |-> Ilk

if
  VGas > 300000

returns Ilk

Mutators

depositing into the system

TODO : add balance ACCT_ID block

behaviour join of ETHJoin
interface join(bytes32 urn)

storage
  // Vat that this adapter points to
  vat |-> Vat
  // collateral type of this adapter
  ilk |-> Ilk

storage Vat
  // whether ACCT_ID is an owner of Vat
  wards[ACCT_ID]      |-> Can
  // unlocked collateral in Ilk assigned to CALLER_ID
  gem[Ilk][CALLER_ID] |-> Rad => Rad + #Ray * VALUE

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000

withdrawing from the system

TODO : add balance ACCT_ID block

behaviour exit of ETHJoin
interface exit(address guy, uint256 wad)

storage
  // Vat that this adapter points to
  vat |-> Vat
  // collateral type of this adapter
  ilk |-> Ilk

storage Vat
  // whether ACCT_ID is an owner of Vat
  wards[ACCT_ID]      |-> Can
  // unlocked collateral in Ilk assigned to CALLER_ID
  gem[Ilk][CALLER_ID] |-> Rad => Rad - #Ray * wad

iff
  // caller is authorised
  Can == 1
  // call stack is not too big
  VCallDepth < 1024
  // there is enough ETH in the adapter
  wad <= BAL

if
  VGas > 300000

DaiJoin

Specification of behaviours

Accessors

vat address

behaviour vat of DaiJoin
interface vat()

storage
  // Vat that this adapter points to
  vat |-> Vat

if
  VGas > 300000

returns Vat

dai address

behaviour dai of DaiJoin
interface dai()

storage
  // underlying dai token of this adapter
  dai |-> Dai

if
  VGas > 300000

returns Dai

Mutators

depositing into the system

behaviour join of DaiJoin
interface join(bytes32 urn, uint256 wad)

storage
  // Vat that this adapter points to
  vat |-> Vat
  // underlying dai token of this adapter
  dai |-> Dai

storage Vat
  // whether ACCT_ID is an owner of Vat
  wards[ACCT_ID] |-> Can
  // dai assigned to CALLER_ID
  dai[CALLER_ID] |-> Rad => Rad + #Ray * wad

storage Dai
  // gem balance of CALLER_ID
  #Gem.balances[CALLER_ID] |-> Bal_guy     => Bal_guy - wad
  // gem balance of ACCT_ID
  #Gem.balances[ACCT_ID]   |-> Bal_adapter => Bal_adapter + wad

iff
  // caller is authorised
  Can == 1
  // call stack is not too big
  VCallDepth < 1024

if
  VGas > 300000

withdrawing from the system

behaviour exit of DaiJoin
interface exit(address guy, uint256 wad)

storage
  // Vat that this adapter points to
  vat |-> Vat
  // underlying dai token of this adapter
  dai |-> Dai

storage Vat
  // whether ACCT_ID is an owner of Vat
  wards[ACCT_ID]      |-> Can
  // unlocked collateral in Ilk assigned to CALLER_ID
  gem[Ilk][CALLER_ID] |-> Rad => Rad - #Ray * wad

storage Dai
  // gem balance of CALLER_ID
  #Gem.balances[CALLER_ID] |-> Bal_guy     => Bal_guy     + wad
  // gem balance of ACCT_ID
  #Gem.balances[ACCT_ID]   |-> Bal_adapter => Bal_adapter - wad

iff
  // caller is authorised
  Can == 1
  // call stack is not too big
  VCallDepth < 1024

if
  VGas > 300000