About Real Time Balance

(NB!! This is a work in progress notes)

Notes

Per Spec

• Real-time balance: vector of liquidity.
  • Current vector components:
    • transferable liquidity (TBA, CFA, GDA, DFA),
    • buffer (CFA),
    • withheld liquidity (GDA),
    • app credit (Buffer Based Solvency).
• Sum of all agreement provided real-time balances.

EVMv1 Implementation Details

• TBA (Transferable Balance Agreement) is not an agreement
• "Settled balance" is a shared storage for:
  • TBA: C,
  • and all constant components of agreement provided real-time balances
    • CFA account: flowRate * time + C
    • IDA subscriber: for s in subs: (s.index.indexValue - s.indexValue) * s.units + C
    • IDA publisher: for i in indexes: i.indexValue * i.totalUnits + C
• Buffer Logic:
  • :Current Logic
  • Clipping is used to store 96 bits as 64 bits
    • CFA: round-up clipping for calculating flow buffer.

Scribbles

	  CLIPPED_MINIMUM_BUFFER = 2**32
Ba = bufferAmount(Fa)

App Credit Rule a:

AppCredit/AppAllowance <= Ba

App Credit Rule b:


## Case 1

Fb + Fc = Fa

Bb = bufferAmount(Fb)
Bc = bufferAmount(Fc)

Worst case:

Bb + Bc = Ba + 2 * (CLIPPED_MINIMUM_BUFFER-1)

## Case 2

Fb + Fc < Fa

Invariances

Liquidity Sum Invariance

• non-semantic money version (CFA, IDA):

forall a. Account a => sum(avb +  (d > od ? d - od : 0)) == totalSupply
  where avb = availableBalance(a)
          d = deposit(a)
         od = owedDeposit(a)

• semantic money version (GDA):

forall a. Account a => sum(availableBalance(a)) == 0

Netflow Sum Invariance

forall a. Account a => sum(netFlowRate(a)) == 0

(Semantic Money/GDA-only) Pool Balance Sum Equals Claimable Balance Sum

forall a p. (Account a, Pool p) => sum(availableBalance(p)) == sum(claimableBalance(a))

(Semantic Money/GDA-only) Flow Buffer Sum Equals Buffer-Account balance

The so called "buffer account" is where the buffer amount is visible as available balance of it. In implementations, they could be the super token contract itself, or in GDA case it could be the GDA agreement contract itself, hypothetically it could be an address of its own such as 0x69.

forall a b. (Account a, BufferAccount b)  => sum(flowBufferAmount(a)) == availableBalance(b)