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

Table of Contents

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. Its methods cannot be called directly, but only through interfaces like Pit and Vow.

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
Vat_wards_succ
SUCCESS

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
Vat_ilks_succ
SUCCESS

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
Vat_urns_succ
SUCCESS

internal unencumbered collateral balances

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

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

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

if
  VGas > 300000

returns Gem
Vat_gem_succ
SUCCESS

internal dai balances

dai is a stablecoin.

behaviour dai of Vat
interface dai(bytes32 guy)

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

if
  VGas > 300000

returns Rad
Vat_dai_succ
SUCCESS

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 guy)

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

if
  VGas > 300000

returns Rad
Vat_sin_succ
SUCCESS

total debt

behaviour debt of Vat
interface debt()

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

if
  VGas > 300000

returns Debt
Vat_debt_succ
SUCCESS

total bad debt

behaviour vice of Vat
interface vice()

storage
  // total system debt
  vice |-> Vice

if
  VGas > 300000

returns Vice
Vat_vice_succ
SUCCESS

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
Vat_deny_succ
SUCCESS
Vat_deny_fail
SUCCESS

initialising an ilk

An ilk starts with Rate and Take set to (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
Vat_init_succ
SUCCESS
Vat_init_fail
SUCCESS

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
Vat_slip_succ
SUCCESS
Vat_slip_fail
SUCCESS

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
Vat_flux_succ
SUCCESS
Vat_flux_fail
SUCCESS

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
Vat_move_succ
SUCCESS
Vat_move_fail
SUCCESS

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
Vat_tune_succ
SUCCESS
Vat_tune_fail
SUCCESS

confiscating a position

When a position of a user u is seized, 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
Vat_grab_succ
SUCCESS
Vat_grab_fail
SUCCESS

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
Vat_heal_succ
SUCCESS
Vat_heal_fail
SUCCESS

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
Vat_fold_succ
SUCCESS
Vat_fold_fail
SUCCESS

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
Vat_toll_succ
SUCCESS
Vat_toll_fail
SUCCESS

Drip

Drip updates each collateral type's debt unit rate while the offsetting dai is supplied to/by a vow. The effect of this is to apply interest to outstanding positions.

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
Drip_wards_succ
SUCCESS

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
Drip_ilks_succ
SUCCESS

vat address

behaviour vat of Drip
interface vat()

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

if
  VGas > 300000

returns Vat
Drip_vat_succ
SUCCESS

vow address

behaviour vow of Drip
interface vow()

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

if
  VGas > 300000

returns Vow
Drip_vow_succ
SUCCESS

global interest rate

behaviour repo of Drip
interface repo()

storage
  // base interest rate
  repo |-> Repo

if
  VGas > 300000

returns Repo
Drip_repo_succ
SUCCESS

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
Drip_deny_succ
SUCCESS
Drip_deny_fail
SUCCESS

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
Drip_init_succ
SUCCESS
Drip_init_fail
SUCCESS

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)

iff
  // caller is authorised
  Can == 1

if
  VGas > 300000
Drip_file_succ
SUCCESS
Drip_file_fail
SUCCESS

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
Drip_file-repo_succ
SUCCESS
Drip_file-repo_fail
SUCCESS

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
Drip_file-vow_succ
SUCCESS
Drip_file-vow_fail
SUCCESS

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
Drip_drip_succ
???
Drip_drip_fail
???

Pit

The Pit is the user's interface to CDPs. It allows users to manipulate their positions subject to certain set conditions intended to limit the system's risk.

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
Pit_wards_succ
SUCCESS

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
Pit_ilks_succ
SUCCESS

liveness

behaviour live of Pit
interface live()

storage
  // system liveness
  live |-> Live

if
  VGas > 300000

returns Live
Pit_live_succ
SUCCESS

vat address

behaviour vat of Pit
interface vat()

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

if
  VGas > 300000

returns Vat
Pit_vat_succ
SUCCESS

global debt ceiling

behaviour Line of Pit
interface Line()

storage
  // global debt ceiling
  Line |-> Line

if
  VGas > 300000

returns Line
Pit_Line_succ
SUCCESS

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
Pit_deny_succ
SUCCESS
Pit_deny_fail
SUCCESS

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
Pit_file-ilk_succ
SUCCESS
Pit_file-ilk_fail
SUCCESS

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
Pit_file-Line_succ
SUCCESS
Pit_file-Line_fail
SUCCESS

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
Pit_frob_succ
???
Pit_frob_fail
???

Vow

The Vow is the system's fiscal organ, the recipient of both system surplus and system debt. Its function is to cover deficits via debt auctions and discharge surpluses via surplus auctions.

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
Vow_wards_succ
SUCCESS

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
Vow_sin_succ
SUCCESS

getting the Sin

behaviour Sin of Vow
interface Sin()

storage
  // total queued sin
  Sin |-> Sin

if
  VGas > 300000

returns Sin
Vow_Sin_succ
SUCCESS

getting the Ash

behaviour Ash of Vow
interface Ash()

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

if
  VGas > 300000

returns Ash
Vow_Ash_succ
SUCCESS

getting the wait

behaviour wait of Vow
interface wait()

storage
  // sin maturation time
  wait |-> Wait

if
  VGas > 300000

returns Wait
Vow_wait_succ
SUCCESS

getting the sump

behaviour sump of Vow
interface sump()

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

if
  VGas > 300000

returns Sump
Vow_sump_succ
SUCCESS

getting the bump

behaviour bump of Vow
interface bump()

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

if
  VGas > 300000

returns Bump
Vow_bump_succ
SUCCESS

getting the hump

behaviour hump of Vow
interface hump()

storage
  // surplus dai cushion
  hump |-> Hump

if
  VGas > 300000

returns Hump
Vow_hump_succ
SUCCESS

getting the Awe

behaviour Awe of Vow
interface Awe()

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

storage Vat
  // system debt assigned to ACCT_ID
  sin[ACCT_ID] |-> Sin

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

if
  VGas > 300000

returns Sin / #Ray
Vow_Awe_succ
SUCCESS
Vow_Awe_fail
SUCCESS

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
Vow_Joy_succ
SUCCESS
Vow_Joy_fail
SUCCESS

getting the Woe

behaviour Woe of Vow
interface Woe()

storage
  // Vat that this Vow points to
  vat |-> Vat 
  // total queued sin
  Sin |-> Ssin
  // total sin in debt auctions
  Ash |-> Ash 

storage Vat
  // system debt assigned to ACCT_ID
  sin[ACCT_ID] |-> Sin

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

if
  VGas > 300000

returns (Sin / #Ray - Ssin) - Ash
Vow_Woe_succ
SUCCESS
Vow_Woe_fail
SUCCESS

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
Vow_deny_succ
SUCCESS
Vow_deny_fail
SUCCESS

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
Vow_file-data_succ
SUCCESS
Vow_file-data_fail
SUCCESS

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
Vow_file-addr_succ
???
Vow_file-addr_fail
SUCCESS

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
Vow_kiss_succ
SUCCESS
Vow_kiss_fail
SUCCESS

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

if
  VGas > 300000
Vow_fess_succ
SUCCESS
Vow_fess_fail
SUCCESS

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
  // sin queued at timestamp t
  sin[t] |-> Sin_t => 0

iff
  // sin has matured
  t + Wait <= TIME

if
  VGas > 300000
Vow_flog_succ
SUCCESS
Vow_flog_fail
SUCCESS

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 
  // total queued sin
  Sin  |-> Ssin
  // total sin in debt auctions
  Ash  |-> Ash  => Ash + Sump
  // debt auction lot size
  sump |-> Sump

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

storage Vat
  // dai assigned to ACCT_ID
  dai[ACCT_ID] |-> Dai  
  // system debt assigned to ACCT_ID
  sin[ACCT_ID] |-> Sin_v

iff
  // caller is authorised
  Can == 1
  //
  (Sin_v / #Ray - Ssin) - Ash >= Sump
  // there is at most dust Joy
  Dai < #Ray
  // call stack is not too big
  VCallDepth < 1024

if
  VGas > 300000

returns 1 + Kicks
Vow_flop_succ
SUCCESS
Vow_flop_fail
SUCCESS

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  |-> Ssin
  // 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] |-> Could => 0

storage Cow
  // dai token
  #Flapper.dai                         |-> DaiMove                                             
  // 
  #Flapper.ttl_tau                     |-> #WordPackUInt48UInt48(Ttl, Tau)                     
  // auction counter
  #Flapper.kicks                       |-> Kicks                                                => 1 + Kicks
  // current bid (dai)
  #Flapper.bids[1 + Kicks].bid         |-> Bid_was                                              => 0
  // current lot (gem)
  #Flapper.bids[1 + Kicks].lot         |-> Lot_was                                              => Bump
  // 
  #Flapper.bids[1 + Kicks].guy_tic_end |-> #WordPackAddrUInt48UInt48(Guy_was, Tic_was, End_was) => #WordPackAddrUInt48UInt48(ACCT_ID, Tic_was, TIME + Tau)
  // beneficiary of the auction
  #Flapper.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_v    => Dai_v - #Ray * Bump
  // system debt assigned to ACCT_ID
  sin[ACCT_ID]   |-> Sin_v   
  // dai assigned to Cow
  dai[Cow]       |-> Dai_c    => Dai_c + #Ray * Bump

iff
  // there is enough Joy
  Dai_v / #Ray >= (Sin_v + Bump) + Hump
  // there is no Woe
  (Sin_v / #Ray - Ssin) - Ash == 0
  // DaiMove is authorised to call Vat
  Can_move == 1
  // call stack is not too big
  VCallDepth < 1022

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

returns 1 + Kicks
Vow_flap_succ
???
Vow_flap_fail
???

Cat

The Cat is the system's liquidation agent: it decides when a position is unsafe and allows it to be seized and sent off to auction.

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
Cat_wards_succ
SUCCESS

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
Cat_ilks_succ
SUCCESS

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
Cat_flips_succ
SUCCESS

liquidation counter

behaviour nflip of Cat
interface nflip()

storage
  // flip count
  nflip |-> Nflip

if
  VGas > 300000

returns Nflip
Cat_nflip_succ
SUCCESS

liveness

behaviour live of Cat
interface live()

storage
  // system liveness
  live |-> Live

if
  VGas > 300000

returns Live
Cat_live_succ
SUCCESS

vat address

behaviour vat of Cat
interface vat()

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

if
  VGas > 300000

returns Vat
Cat_vat_succ
SUCCESS

pit address

behaviour pit of Cat
interface pit()

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

if
  VGas > 300000

returns Pit
Cat_pit_succ
SUCCESS

vow address

behaviour vow of Cat
interface vow()

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

if
  VGas > 300000

returns Vow
Cat_vow_succ
SUCCESS

Mutators

adding 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
Cat_deny_succ
SUCCESS
Cat_deny_fail
SUCCESS

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
Cat_file-addr_succ
SUCCESS
Cat_file-addr_fail
SUCCESS

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
Cat_file_succ
SUCCESS
Cat_file_fail
SUCCESS

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
Cat_file-flip_succ
SUCCESS
Cat_file-flip_fail
SUCCESS

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
Cat_bite_succ
???
Cat_bite_fail
???

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
  // 
  #Flipper.ttl_tau                     |-> #WordPackUInt48UInt48(Ttl, Tau)
  // auction counter
  #Flipper.kicks                       |-> Kicks                           => 1 + Kicks
  // current bid (dai)
  #Flipper.bids[1 + Kicks].bid         |-> _                               => 0
  // current lot (gem)
  #Flipper.bids[1 + Kicks].lot         |-> _                               => (Ink * wad) / Tab
  // 
  #Flipper.bids[1 + Kicks].guy_tic_end |-> _                               => #WordPackAddrUInt48UInt48(ACCT_ID, 0, TIME + Tau)
  // beneficiary of remaining gems
  #Flipper.bids[1 + Kicks].urn         |-> _                               => Urn
  // beneficiary of dai
  #Flipper.bids[1 + Kicks].gal         |-> _                               => Vow
  // debt to cover
  #Flipper.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
Cat_flip_succ
???
Cat_flip_fail
???

GemJoin

The GemJoin adapter allows standard ERC20 tokens to be deposited for use with the system.

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
GemJoin_vat_succ
???

the associated ilk

behaviour ilk of GemJoin
interface ilk()

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

if
  VGas > 300000

returns Ilk
GemJoin_ilk_succ
???

gem address

behaviour gem of GemJoin
interface gem()

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

if
  VGas > 300000

returns Gem
GemJoin_gem_succ
???

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
GemJoin_join_succ
???
GemJoin_join_fail
???

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
GemJoin_exit_succ
???
GemJoin_exit_fail
???

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
ETHJoin_vat_succ
???

the associated ilk

behaviour ilk of ETHJoin
interface ilk()

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

if
  VGas > 300000

returns Ilk
ETHJoin_ilk_succ
???

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
ETHJoin_join_succ
???
ETHJoin_join_fail
???

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
ETHJoin_exit_succ
???
ETHJoin_exit_fail
???

DaiJoin

The DaiJoin adapter allows users to withdraw their dai from the system into a standard ERC20 token.

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
DaiJoin_vat_succ
???

dai address

behaviour dai of DaiJoin
interface dai()

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

if
  VGas > 300000

returns Dai
DaiJoin_dai_succ
???

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
DaiJoin_join_succ
???
DaiJoin_join_fail
???

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
DaiJoin_exit_succ
???
DaiJoin_exit_fail
???

DaiMove

The DaiMove provides a minimal interface for transferring internal dai balances and granting transfer approval to other accounts.

Specification of behaviours

Accessors

the Vat

behaviour vat of DaiMove
interface vat()

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

if
  VGas > 300000

returns Vat
DaiMove_vat_succ
SUCCESS

Mutators

approve or unapprove an address

behaviour nope of DaiMove
interface nope(address guy)

storage
  // guy is authorised to move for CALLER_ID
  can[CALLER_ID][guy] |-> Could => 0

if
  VGas > 300000
DaiMove_nope_succ
SUCCESS

move tokens

behaviour move of DaiMove
interface move(address src, address dst, uint256 wad)

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

storage Vat
  // whether ACCT_ID is an owner of Vat
  wards[ACCT_ID] |-> Can_move
  // dai assigned to src
  dai[src]       |-> Dai_src  => Dai_src - #Ray * wad
  // dai assigned to dst
  dai[dst]       |-> Dai_dst  => Dai_dst + #Ray * wad

iff
  // caller is approved to move tokens
  ((src == CALLER_ID) or (Can == 1))
  // call stack not too big
  VCallDepth < 1024
  // DaiMove authorised to call Cat
  Can_move == 1

if
  VGas > 300000
DaiMove_move_succ
SUCCESS
DaiMove_move_fail
SUCCESS

Flapper

The Flapper is an auction contract that receives dai tokens and starts an auction, accepts bids of gem (with tend), and after completion settles with the winner.

Specification of behaviours

Accessors

bid data

behaviour bids of Flapper
interface bids(uint256 n)

storage
  // current bid (dai)
  bids[n].bid         |-> Bid                                     
  // current lot (gem)
  bids[n].lot         |-> Lot                                     
  // 
  bids[n].guy_tic_end |-> #WordPackAddrUInt48UInt48(Guy, Tic, End)
  // beneficiary of the auction
  bids[n].gal         |-> Gal                                     

if
  VGas > 300000

returns Bid : Lot : #WordPackAddrUInt48UInt48(Guy, Tic, End) : Gal
Flapper_bids_succ
???

sell token

behaviour dai of Flapper
interface dai()

storage
  // dai token
  dai |-> Dai

if
  VGas > 300000

returns Dai
Flapper_dai_succ
SUCCESS

buy token

behaviour gem of Flapper
interface gem()

storage
  // mkr token
  gem |-> Gem

if
  VGas > 300000

returns Gem
Flapper_gem_succ
???

minimum bid increment

behaviour beg of Flapper
interface beg()

storage
  // minimum bid increment
  beg |-> Beg

if
  VGas > 300000

returns Beg
Flapper_beg_succ
???

auction time-to-live

behaviour ttl of Flapper
interface ttl()

storage
  // 
  ttl_tau |-> #WordPackUInt48UInt48(Ttl, Tau)

if
  VGas > 300000

returns Ttl
Flapper_ttl_succ
???

maximum auction duration

behaviour tau of Flapper
interface tau()

storage
  // 
  ttl_tau |-> #WordPackUInt48UInt48(Ttl, Tau)

if
  VGas > 300000

returns Tau
Flapper_tau_succ
???

kick counter

behaviour kicks of Flapper
interface kicks()

storage
  // auction counter
  kicks |-> Kicks

if
  VGas > 300000

returns Kicks
Flapper_kicks_succ
???

Mutators

starting an auction

behaviour kick of Flapper
interface kick(address gal, uint256 lot, uint256 bid)

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

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

storage Vat
  // whether DaiMove is an owner of Vat
  wards[DaiMove] |-> Can_move
  // dai assigned to CALLER_ID
  dai[CALLER_ID] |-> Dai_v    => Dai_v - #Ray * lot
  // dai assigned to ACCT_ID
  dai[ACCT_ID]   |-> Dai_c    => Dai_c + #Ray * lot

iff
  // call stack is not too big
  VCallDepth < 1023
  // Flap is authorised to move for the caller
  Can      == 1
  // DaiMove is authorised to call Vat
  Can_move == 1

if
  CALLER_ID =/= ACCT_ID
  VGas > 300000

returns 1 + Kicks
Flapper_kick_succ
???
Flapper_kick_fail
???