What follows is an executable K specification of the smart contracts of multicollateral dai.
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.
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
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
dataAn 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
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
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
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
behaviour debt of Vat
interface debt()
storage
// total dai issued from the system
debt |-> Debt
if
VGas > 300000
returns Debt
behaviour vice of Vat
interface vice()
storage
// total system debt
vice |-> Vice
if
VGas > 300000
returns Vice
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
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
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
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
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
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
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
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
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
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
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.
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
databehaviour 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
addressbehaviour vat of Drip
interface vat()
storage
// Vat that this Drip points to
vat |-> Vat
if
VGas > 300000
returns Vat
vow
addressbehaviour vow of Drip
interface vow()
storage
// Vow that this Drip points to
vow |-> Vow
if
VGas > 300000
returns Vow
behaviour repo of Drip
interface repo()
storage
// base interest rate
repo |-> Repo
if
VGas > 300000
returns Repo
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
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
ilk
databehaviour 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
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
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
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
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.
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
databehaviour 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
behaviour live of Pit
interface live()
storage
// system liveness
live |-> Live
if
VGas > 300000
returns Live
vat
addressbehaviour vat of Pit
interface vat()
storage
// Vat that this Pit points to
vat |-> Vat
if
VGas > 300000
returns Vat
behaviour Line of Pit
interface Line()
storage
// global debt ceiling
Line |-> Line
if
VGas > 300000
returns Line
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
ilk
databehaviour 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
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
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
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.
behaviour wards of Vow
interface wards(address guy)
storage
// whether guy is an owner of Vow
wards[guy] |-> Can
if
VGas > 300000
returns Can
sin
packetbehaviour sin of Vow
interface sin(uint48 era)
storage
// sin queued at timestamp era
sin[era] |-> Sin_era
if
VGas > 300000
returns Sin_era
Sin
behaviour Sin of Vow
interface Sin()
storage
// total queued sin
Sin |-> Sin
if
VGas > 300000
returns Sin
Ash
behaviour Ash of Vow
interface Ash()
storage
// total sin in debt auctions
Ash |-> Ash
if
VGas > 300000
returns Ash
wait
behaviour wait of Vow
interface wait()
storage
// sin maturation time
wait |-> Wait
if
VGas > 300000
returns Wait
sump
behaviour sump of Vow
interface sump()
storage
// debt auction lot size
sump |-> Sump
if
VGas > 300000
returns Sump
bump
behaviour bump of Vow
interface bump()
storage
// surplus auction lot size
bump |-> Bump
if
VGas > 300000
returns Bump
hump
behaviour hump of Vow
interface hump()
storage
// surplus dai cushion
hump |-> Hump
if
VGas > 300000
returns Hump
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
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
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
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
parametersbehaviour 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
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
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
sin
queuebehaviour 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
sin
queuebehaviour 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
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
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
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.
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
databehaviour 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
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
behaviour nflip of Cat
interface nflip()
storage
// flip count
nflip |-> Nflip
if
VGas > 300000
returns Nflip
behaviour live of Cat
interface live()
storage
// system liveness
live |-> Live
if
VGas > 300000
returns Live
vat
addressbehaviour vat of Cat
interface vat()
storage
// Vat that this Cat points to
vat |-> Vat
if
VGas > 300000
returns Vat
pit
addressbehaviour pit of Cat
interface pit()
storage
// Pit that this Cat points to
pit |-> Pit
if
VGas > 300000
returns Pit
vow
addressbehaviour vow of Cat
interface vow()
storage
// Vow that this Cat points to
vow |-> Vow
if
VGas > 300000
returns Vow
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
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
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
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
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
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
The GemJoin
adapter allows standard ERC20 tokens to be deposited for use with the system.
vat
addressbehaviour vat of GemJoin
interface vat()
storage
// Vat that this adapter points to
vat |-> Vat
if
VGas > 300000
returns Vat
ilk
behaviour ilk of GemJoin
interface ilk()
storage
// collateral type of this adapter
ilk |-> Ilk
if
VGas > 300000
returns Ilk
behaviour gem of GemJoin
interface gem()
storage
// underlying token of this adapter
gem |-> Gem
if
VGas > 300000
returns Gem
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
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
vat
addressbehaviour vat of ETHJoin
interface vat()
storage
// Vat that this adapter points to
vat |-> Vat
if
VGas > 300000
returns Vat
ilk
behaviour ilk of ETHJoin
interface ilk()
storage
// collateral type of this adapter
ilk |-> Ilk
if
VGas > 300000
returns Ilk
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
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
The DaiJoin
adapter allows users to withdraw their dai from the system into a standard ERC20 token.
vat
addressbehaviour vat of DaiJoin
interface vat()
storage
// Vat that this adapter points to
vat |-> Vat
if
VGas > 300000
returns Vat
behaviour dai of DaiJoin
interface dai()
storage
// underlying dai token of this adapter
dai |-> Dai
if
VGas > 300000
returns Dai
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
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
The DaiMove
provides a minimal interface for transferring internal dai balances and granting transfer approval to other accounts.
behaviour vat of DaiMove
interface vat()
storage
// Vat that this DaiMove points to
vat |-> Vat
if
VGas > 300000
returns Vat
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
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
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.
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
behaviour dai of Flapper
interface dai()
storage
// dai token
dai |-> Dai
if
VGas > 300000
returns Dai
behaviour gem of Flapper
interface gem()
storage
// mkr token
gem |-> Gem
if
VGas > 300000
returns Gem
behaviour beg of Flapper
interface beg()
storage
// minimum bid increment
beg |-> Beg
if
VGas > 300000
returns Beg
behaviour ttl of Flapper
interface ttl()
storage
//
ttl_tau |-> #WordPackUInt48UInt48(Ttl, Tau)
if
VGas > 300000
returns Ttl
behaviour tau of Flapper
interface tau()
storage
//
ttl_tau |-> #WordPackUInt48UInt48(Ttl, Tau)
if
VGas > 300000
returns Tau
behaviour kicks of Flapper
interface kicks()
storage
// auction counter
kicks |-> Kicks
if
VGas > 300000
returns Kicks
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