Skip to content

Numerical Ranges

Kurt Barry edited this page Jun 21, 2021 · 38 revisions

Background

As a consequence of using finite-precision arithmetic, the contracts in this repository will only work well if the magnitudes of various values are within reasonable bounds. This document defines what these boundaries are intended to be; i.e. any contract that performs incorrectly (for example, reverting due to an overflow or arriving at an inaccurate result due to round-off error) for input values that are all within the ranges given here should be considered flawed. These values are subject to revision and may be overly-conservative (i.e. the system may in fact function correctly even when some values stray from these ranges).

Notation

Ranges are given in the form:

Lower_Bound <= Quantity <= Upper_Bound

Rarely, strict inequality (< instead of <=) may apply to one or both of the bounds.

Some ranges will depend wholly or partially on the upper and/or lower bounds of other quantities. The notation L(Quantity) will denote the lower bound of Quantity, and the notation U(Quantity) will denote the upper bound of Quantity.

Constants:

WAD = 10^18
RAY = 10^27
RAD = 10^45

Bounds

1. Implementation-Independent Values

These are quantities that would exist regardless of the implementation of the system, and are expressed 18 decimal fixed-point notation for convenience.

1.1 Total DAI Market Cap (US Dollars as 18 decimal fixed point)

10^16 <= Total_DAI_MC_Dollars <= 10^32

1.2 Per-Token Collateral Price (US Dollars as 18 decimal fixed point)

10^12 <= PerToken_Collateral_Price_Dollars <= 10^30

1.3 DAI Price (in US Dollars as 18 decimal fixed point)

This is the actual price DAI trades at on the open market, and determines the value reported by any oracle

5 * 10^17 <= DAI_Price_Dollars <= 2 * 10^18

1.4 Total DAI Supply (18 decimal fixed point)

WAD * L(Total_DAI_MC_Dollars) / U(DAI_Price_Dollars) <= Total_DAI_Supply <= WAD * U(Total_DAI_MC_Dollars) / L(DAI_Price_Dollars)

Substituting values, we obtain:

5 * 10^15 <= Total_DAI_Supply <= 2 * 10^32

1.5 ERC20 totalSupply

0 < ERC20_totalSupply <= 10^20 * WAD == 10^38

1.6 MKR Price DAI (in 18 decimal fixed point)

10^16 <= MKR_Price_DAI <= 10^24

2. Implementation-Dependent Values

These are quantities defined in the specific smart contracts found in this repository. Most of the bounds are at least partially derived from the system-independent values, and all non-integer expressions should be assumed to be truncated to the nearest integer.

2.1 Spotter

2.1.1 Spotter.par

Currently, we are not interested in considering values of Spotter.par that deviate from unity (in fixed-point representation).

10^27 <= Spotter.par <= 10^27

2.1.2 Spotter.Ilk.mat

10^27 <= Spotter.Ilk.mat <= 10^31

2.2 Vat

2.2.1 Vat.debt

L(Total_DAI_Supply) * RAY <= Vat.debt <= U(Total_DAI_Supply) * RAY

Substituting values, we obtain:

5 * 10^42 <= Vat.debt <= 2 * 10^59

2.2.2 Vat.vice

0 <= Vat.vice <= U(Vat.debt)

Substituting:

0 <= Vat.vice <= 2 * 10^59

2.2.3 Vat.Line

0 <= Vat.Line <= 2^256 - 1

2.2.4 Vat.Ilk.rate

Upper bound derived by assuming a 50% APY for 50 years.

10^27 <= Vat.Ilk.rate <= 64 * 10^34

2.2.5 Vat.Ilk.Art

0 <= Vat.Ilk.Art <= U(Vat.debt) / L(Vat.Ilk.rate)

Substituting values, we obtain:

0 <= Vat.Ilk.Art <= 2 * 10^42

2.2.6 Vat.Ilk.spot

( RAY * RAY * 10^9 * L(PerToken_Collateral_Price_Dollars) ) / ( U(Spotter.par) * U(Spotter.Ilk.mat) )
<=
Vat.Ilk.spot
<=
( RAY * RAY * 10^9 * U(PerToken_Collateral_Price_Dollars) ) / ( L(Spotter.par) * L(Spotter.Ilk.mat) )

Substituting values:

10^17 <= Vat.Ilk.spot <= 10^39

2.2.7 Vat.Ilk.line

0 <= Vat.Ilk.line <= 2^256 - 1

2.2.8 Vat.Ilk.dust

Strict inequality on lower bound is intentional.

0 < Vat.Ilk.dust <= 10^5 * RAD * WAD / L(DAI_Price_Dollars)

Substituting values:

0 < Vat.Ilk.dust <= 2 * 10^50

2.2.9 Vat.Urn.ink

0 <= Vat.Urn.ink <= ERC20_totalSupply

Substituting:

0 <= Vat.Urn.ink <= 10^38

2.2.10 Vat.Urn.art

0 <= Vat.Urn.art <= U(Vat.Ilk.Art)

Substituting:

0 <= Vat.Urn.art <= 2 * 10^42

2.2.11 Vat.gem[u]

0 <= Vat.gem[u] <= U(ERC20_totalSupply)

Substituting:

0 <= Vat.gem[u] <= 10^38

2.2.12 Vat.dai[u]

0 <= Vat.dai[u] <= U(Vat.debt)

Substituting:

0 <= Vat.dai[u] <= 2 * 10^59

2.2.13 Vat.sin[u]

0 <= Vat.sin[u] <= U(Vat.vice)

Substituting:

0 <= Vat.sin[u] <= 2 * 10^59

2.3 Jug

Jug.Ilk.duty

UB is 100% APY

10^27 <= duty <= 1000000022535216018065179047

Jug.Ilk.rho

From MCD launch to 50 years in the future.

1574092804 <= Jug.Ilk.rho <= 3151972804

2.4 Pot

2.4.1 Pot.chi

Upper bound derived by assuming a 50% APY for 50 years.

10^27 <= Vat.Ilk.rate <= 64 * 10^34

2.4.2 Pot.Pie

0 <= Pot.Pie <= U(Vat.debt) / L(Pot.chi)

Substituting:

0 <= Pot.Pie <= 2 * 10^32

2.4.3 Pot.pie[u]

0 <= Pot.pie[u] <= U(Pot.Pie)

Substituting:

0 <= Pot.pie[u] <= 2 * 10^32

2.4.4 Pot.dsr

UB is 100% APY

RAY <= Pot.dsr <= 1000000022535216018065179047

2.4.5 Pot.rho

From MCD launch to 50 years in the future.

1574092804 <= Pot.rho <= 3151972804

2.5 Vow

2.5.1 Vow.sin[t]

0 <= Vow.sin[t] <= U(Vat.vice)

Substituting:

0 <= Vow.sin[t] <= 2 * 10^59

2.5.2 Vow.Sin

0 <= Vow.Sin <= U(Vat.vice)

Substituting:

0 <= Vow.Sin <= 2 * 10^59

2.5.3 Vow.Ash

0 <= Vow.Ash <= U(Vat.vice)

Substituting:

0 <= Vow.Ash <= 2 * 10^59

2.5.4 Vow.wait

Between 1 hour and 28 days.

3600 <= Vow.wait <= 2419200

2.5.5 Vow.sump

10^46 <= Vow.sump <= 10^51

2.5.6 Vow.dump

L(Vow.sump) / U(MKR_Price_DAI) / 10^9 <= Vow.dump <= U(Vow.sump) / L(MKR_Price_DAI) / 10^9

Substituting:

10^13 <= Vow.dump <= 10^34

2.5.7 Vow.bump

10^46 <= Vow.bump <= 10^51

2.5.8 Vow.hump

0 <= Vow.hump <= RAY * U(Total_DAI_Supply) / 100

Substituting:

0 <= Vow.hump <= 2 * 10^57

Cat

Cat.Ilk.chop

0 to 20% liquidation penalty.

10^18 <= Cat.Ilk.chop <= 12 * 10^17

Cat.Ilk.lump (deprecated)

Strict lower bound intentional.

0 < Cat.Ilk.lump <= 10^6 * WAD * U(DAI_Price_Dollars) / L(PerToken_Collateral_Price_Dollars

Substituting:

0 < Cat.Ilk.lump <= 2 * 10^30

Cat.Ilk.dunk

Strict lower bound intentional.

0 < Cat.Ilk.dunk <= 10^6 * RAD

Substituting:

0 < Cat.Ilk.dunk <= 10^51

Cat.box

0 <= Cat.box <= U(Vat.debt)

Substituting:

0 <= Cat.box <= 2 * 10^59

Cat.litter

0 <= Cat.litter <= U(Cat.box)

Substituting:

0 <= Cat.litter <= 2 * 10^59

Dog

Dog.Ilk.chop

0 to 20% liquidation penalty.

10^18 <= Dog.Ilk.chop <= 12 * 10^17

Dog.Ilk.hole

0 <= Dog.Ilk.hole <= U(Vat.debt)

Substituting:

0 <= Dog.Ilk.hole <= 2 * 10^59

Dog.Ilk.dirt

0 <= Dog.Ilk.dirt <= Dog.Ilk.hole

Substituting:

0 <= Dog.Ilk.dirt <= 2 * 10^59

Dog.Hole

0 <= Dog.Hole <= U(Vat.debt)

Substituting:

0 <= Dog.Hole <= 2 * 10^59

Dog.Dirt

0 <= Dog.Dirt <= U(Dog.Hole)

Substituting:

0 <= Dog.Dirt <= 2 * 10^59

Flipper

Flipper.Bid.bid

0 <= Flipper.Bid.bid <= U(Flipper.Bid.tab)

Substituting:

0 <= Flipper.Bid.bid <= 12 * 10^50

Flipper.Bid.lot

Strict lower bound intentional

0 < Flipper.Bid.lot <= U(Cat.Ilk.dunk) * U(DAI_Price_Dollars) / ( L(PerToken_Collateral_Price_Dollars) * RAY )

Substituting:

0 < Flipper.Bid.lot <= 2 * 10^30

Flipper.Bid.tic

Nov 1st 2019 to Nov 1st 2069

1572566400 <= Flipper.Bid.tic <= 3150489600

Flipper.Bid.end

Nov 1st 2019 to Nov 1st 2069

1572566400 <= Flipper.Bid.end <= 3150489600

Flipper.Bid.tab

Strict lower bound intentional.

0 < Flipper.Bid.tab <= U(Cat.Ilk.dunk) * U(Cat.Ilk.chop) / WAD

Substituting:

0 < Flipper.Bid.tab <= 12 * 10^50

Flipper.beg

Strict lower bound intentional.

WAD < Flipper.beg <= 11 * 10^17

Flipper.ttl

1 minute to max auction lifetime.

60 <= Flipper.ttl <= U(Flipper.tau)

Substituting:

360 <= Flipper.ttl <= 2592000

Flipper.tau

5 minutes to one month.

360 <= Flipper.tau <= 2592000

Flipper.kicks

Upper bound is roughly a million auctions per day for 50 years.

0 < Flipper.kicks <= 2 * 10^10

Clipper

Clipper.buf

1x to 3x OSM price

RAY <= Clipper.buf <= 3 * RAY

Clipper.tail

5 minutes to 1 month

360 <= Clipper.tail <= 2592000

Clipper.cusp

1% to 99%

RAY / 100 <= Clipper.cusp <= 99 * RAY / 100

Clipper.chip

Clipper.tip

Clipper.chost

Strict lower bound intentional.

L(Vat.Ilk.dust) * L(Dog.Ilk.chop) / WAD < Clipper.chost <= U(Vat.Ilk.dust) * U(Dog.Ilk.chop) / WAD

Substituting:

0 < Clipper.chost <= 24 * 10^49

Clipper.Sale.tab

Strict lower bound intentional.

0 < Clipper.Sale.tab <= U(Vat.debt)

Substituting:

0 < Clipper.Sale.tab <= 2 * 10^59

Clipper.Sale.lot

Strict lower bound intentional.

0 < Clipper.Sale.lot <= U(Clipper.Sale.tab) * U(DAI_Price_Dollars) / ( L(PerToken_Collateral_Price_Dollars) * RAY )

Substituting:

0 < Clipper.Sale.lot <= 4 * 10^38

Clipper.Sale.tic

Nov 1st 2019 to Nov 1st 2069

1572566400 <= Clipper.Sale.tic <= 3150489600

Clipper.Sale.top

L(PerToken_Collateral_Price_Dollars) * L(Clipper.buf) / WAD <= Clipper.Sale.top <= U(PerToken_Collateral_Price_Dollars) * U(Clipper.buf) / WAD

Substituting:

10^19 <= Clipper.Sale.top <= 3 * 10^39

StairstepExponentialDecrease

StairstepExponentialDecrease.step

15 sec to 10 min

15 <= StairstepExponentialDecrease.step <= 600

StairstepExponentialDecrease.cut

0 < StairstepExponentialDecrase.cut < RAY

Flapper

Flapper.Bid.bid

Assuming a floor MKR price of 0.001 DAI.

0 <= Flapper.Bid.bid <= U(Flapper.Bid.lot) / (10^15 * 10^9)

Substituting:

0 <= Flapper.Bid.bid <= 10^26

Flapper.Bid.lot

0 < Flapper.Bid.lot <= 10^6 * RAD

Flapper.Bid.tic

Nov 1st 2019 to Nov 1st 2069

1572566400 <= Flapper.Bid.tic <= 3150489600

Flapper.Bid.end

Nov 1st 2019 to Nov 1st 2069

1572566400 <= Flapper.Bid.end <= 3150489600

Flapper.beg

Strict lower bound intentional.

WAD < Flapper.beg <= 11 * 10^17

Flapper.ttl

1 minute to max auction lifetime.

60 <= Flapper.ttl <= U(Flapper.tau)

Flapper.tau

5 minutes to one month.

360 <= Flapper.tau <= 2592000

Flapper.kicks

Upper bound is roughly a million auctions per day for 50 years.

0 < Flapper.kicks <= 2 * 10^10

Flopper

Flopper.Bid.bid

0 < Flopper.Bid.bid <= 10^6 * RAD

Flopper.Bid.lot

Assuming a floor MKR price of 0.001 DAI.

0 <= Flopper.Bid.lot <= U(Flopper.Bid.bid) / (10^15 * 10^9)

Substituting:

0 <= Flopper.Bid.lot <= 10^26

Flopper.Bid.tic

Nov 1st 2019 to Nov 1st 2069

1572566400 <= Flopper.Bid.tic <= 3150489600

Flopper.Bid.end

Nov 1st 2019 to Nov 1st 2069

1572566400 <= Flopper.Bid.end <= 3150489600

Flopper.beg

Strict lower bound intentional.

WAD < Flopper.beg <= 11 * 10^17

Flopper.pad

Strict lower bound intentional.

WAD < Flapper.pad <= 4 * 10^18

Flopper.ttl

1 minute to max auction lifetime.

60 <= Flopper.ttl <= U(Flapper.tau)

Flopper.tau

5 minutes to one month.

360 <= Flopper.tau <= 2592000

Flopper.kicks

Upper bound is roughly a million auctions per day for 50 years.

0 < Flopper.kicks <= 2 * 10^10

End

End.when

Nov 1st 2019 to Nov 1st 2069

1572566400 <= End.when <= 3150489600

End.wait

Up to one week.

0 <= End.wait <= 14515200

End.debt

L(Vat.debt) < End.debt <= U(Vat.debt)

Substituting:

5 * 10^42 < End.debt <= 2 * 10^59

Eng.tag[i]

L(Spotter.par) * WAD / U(PerToken_Collateral_Price_Dollars) <= End.tag[i] <= U(Spotter.par) * WAD / L(PerToken_Collateral_Price_Dollars)

Substituting:

10^15 <= End.tag[i] <= 10^33

End.gap[i]

0 <= End.gap[i] <= U(Vat.debt) / (10^9 * L(PerToken_Collateral_Price_Dollars))

Substituting:

0 <= End.gap[i] <= 2 * 10^38

End.Art[i]

0 <= End.Art[i] <= U(Vat.debt) / L(Vat.Ilk.rate)

Substituting:

0 <= End.Art[i] <= 2 * 10^32

End.fix[i]

0 < End.fix[i] <= U(End.tag[i])

Substituting:

0 < End.fix[i] <= 10^33

End.bag[u]

0 <= End.bag[u] <= U(Vat.debt) / RAY

Substituting:

0 <= End.bag[u] <= 2 * 10^32

End.out[i][u]

0 <= End.out[i][u] <= U(Vat.debt) / (10^9 * L(PerToken_Collateral_Price_Dollars))

Substituting:

0 <= End.out[i][u] <= 2 * 10^38
Clone this wiki locally