spec.md

Contracts

• Vat
  • Heal
• Vow
  • Heal

Vat

Description and comments go here. All headings as below can be referenced. manipulating bad debt and surplus

behaviour heal of Vat

interface heal(bytes32 u, bytes32 v, int256 rad)

types

    Can   : uint256
    Dai_v : uint256
    Sin_u : uint256
    Debt  : uint256
    Vice  : uint256

storage

    #Vat.wards(CALLER_ID) |-> Can
    #Vat.dai(v)           |-> Dai_v => Dai_v - rad
    #Vat.sin(u)           |-> Sin_u => Sin_u - rad
    #Vat.debt             |-> Debt  => Debt - rad
    #Vat.vice             |-> Vice  => Vice - rad

iff

    Can == 1

iff in range uint256

    Dai_v - rad
    Sin_u - rad
    Debt - rad
    Vice - rad

other vat functions

Vow

cancelling bad debt and surplus

behaviour heal of Vow

behaviour heal of Vow
interface heal(uint256 wad)

types

    Can  : uint256
    Vat  : address VatLike
    Woe  : uint256
    Dai  : uint256
    Sin  : uint256
    Vice : uint256
    Debt : uint256

storage

    #Vow.vat |-> Vat
    #Vow.Woe |-> Woe => Woe - wad

storage Vat
    
    #Vat.wards(ACCT_ID) |-> Can
    #Vat.dai(ACCT_ID)   |-> Dai  => Dai - #Ray * wad
    #Vat.sin(ACCT_ID)   |-> Sin  => Sin - #Ray * wad
    #Vat.vice           |-> Vice => Vice - #Ray * wad
    #Vat.debt           |-> Debt => Debt - #Ray * wad

iff

    Can == 1
    wad <= Dai / 1000000000000000000000000000
    wad <= Woe

iff in range uint256

    Woe - wad
    Dai - #Ray * wad
    Sin - #Ray * wad
    Vice - #Ray * wad
    Debt - #Ray * wad
    
iff in range int256

    #Ray * wad

Calls Vat.Heal