Numerical Ranges

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 / L(DAI_Price_Dollars)

Substituting values:

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

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

Dog

Flipper

Clipper

StairstepExponentialDecrease

Flapper

Flopper

End