k-dss higher invariants

Vat invariants

Some invariants
\[\Sigma_u({\tt art_{iu}}) = {\tt Art_i}\]

\[\Sigma_u({\tt ink_{iu}}) = {\tt Ink_i}\]

\[\Sigma_u({\tt dai_u}) = {\tt debt}\]

\[\Sigma_u({\tt sin_u}) = {\tt vice}\]

CDP debt + system debt = total dai supply [the fundamental equation of dai].
\[\Sigma_{i}({\tt rate_i} \cdot \Sigma_{u}({\tt art_{iu}})) + \Sigma_{u}({\tt sin_{u}})= \Sigma_u({\tt dai_u})\]
or, in other words
\[\Sigma_{i}({\tt rate_i} \cdot {\tt Art_{i}}) + \tt vice = \tt debt\]

Global invariants

The following equation holds "morally"; nothing really stops people from sending collateral to the adapter without receiving a corresponding Gem balance. But the equation holds if we understand balanceOf to measure the collateral that has been sent to the adapter through the join function.

Unlocked collateral + locked collateral = all collateral

The balance of the Gem adapter contract = free collateral + locked collateral units * the price. For every ilk, i, have:
\[{\tt take}\cdot\Sigma_{u}({\tt ink_{iu}}) + 10^{27}\cdot\Sigma_{u}({\tt gem_{iu}}) = 10^{27} \cdot \tt balanceOf(\tt GemJoin_i) \]

All of the above can be proved by induction and case analysis on the methods in Vat.

Liquidation invariants

\[{\tt take}\cdot\Sigma_{u}({\tt ink_{iu}}) + \cdot\Sigma_{u}({\tt gem_{iu}}) = \tt balanceOf(\tt GemJoin_i) \]