# Superfluid Tech Deep Dives - Maths of Generalized Distribution Agreements

## 1. Generalized Distribution Payment Semantics

Think of the following hypothetical payment requests:

- Microsoft requests to send $0.42 per share to all its share holders
*on the next ex-dividend date*. - Elon Musk requests to send a constant flow of money at â‚¬4.2B per 360 days to all its share holders with individual
flow rates proportional to their number of share units,
*from 20st April*.

How do we perform these payment requests in a payment system in a way that there are as least amount messages (transactions) happening as possible?

And this is the central question to the design of the generalized distribution agreements, and those are the examples of
its payment semantics^{1}.

In this article we will go through some maths in its specification.

## 2. General Constructions

The key concepts of a distribution agreement are: *publishers*, *subscribers* and *indexes*, whereby:

- A publisher distributes money through a index to the subscribers of the index.
- An index records proportions of distributions at which each of its subscribers should receive.

### 2.1. Proportional Distribution and Units

For the purpose of this article, the index is limited to being *proportional distribution index*. In this form, each
subscriber subscribes to a number of *units* of the index. And number of units determines the proportional amounts
subscribers should receive from the distributions. You can think of dividend payments from Microsoft to its share
holders is such example, where the number of shares at ex-div date determines your dividend payout amount at the payout
date.

The name of the semantic function for subscribers is `updateSubscription`

.

### 2.2. Distribution Curve

The function of which how the publisher distributes money is the *distribution curve*.

Distribution curve can be any arbitrary continuous function, but for a practical solvency response system (in this case, a system that can check if the publisher still have positive balance left), it is desirable to have a distribution curve that is monotonically non-decreasing.

However, instant distribution is a special case even though it is not a continuous function. It can still work because
it doesn't have a curve at all hence some specialization in implementation could be done to accommodate that fact. The
name of the semantic function for the publisher of a instant distribution index is `distributeValue`

.

For the purpose of this article, we will also explore the constant flow distribution curve, where publisher distribute
one big flow at a constant flow rate to all its subscribers, where subscribers proportionally gets smaller flows
according to their number of units. The name of the semantic function for the publisher of a constant flow distribution
index is `updateConstantFlowDistributionRate`

.

### 2.3. Computation Complexity

On a note of space complexity, for a publisher, the cost of storing its indexes is constant `O(1).`

But for the
subscribers, it is rather of linear `O(N)`

, for reasons this article will not elaborate more on.

Since to calculate current balance of a subscriber, it is necessary to iterate through all its subscriptions, the time complexity story is the same for subscribers.

### 2.4. General Principles

**Common variables**

`t_s`

: settled at`sv`

: settled value

**Variables for publisher**

`vpu`

: value per unit (of the index).

**Variable For subscriber**

`svpu`

: settled value per unit (of each subscriber).

How these variables are updated:

- Publisher
`vpu`

is always updated for either a publisher operation (`distributeFlow`

, or`updateConstantFlowDistribution`

) or a subscriber operation (`updateSubscription`

units). - Publisher's balance curve is indistinguishable between sending to 1 participant to N subscribers. This observation
also leads to the design of using "lens abstraction"
^{2}when defining the specification. - A subscriber's
`svpu`

is updated only when a subscriber operation applied to it.

## 3. Instant Distribution Operations

Let's first have a look how the instant distribution index work for its operations (`updateSubscription`

&
`distributeValue`

). This will solve the puzzle of how can Microsoft sends dividends to all its shareholders using the
least amount of transactions.

### 3.1. Publisher Balance Function

Per principle (2), balance function for publisher is the same as a simple 1 to 1 instant transfer, which is simply a constant function of a fixed value settled per principle (1).

### 3.2. Subscriber Balance Function

Balance function for subscriber is:

sv + floor (u * fromIntegral (vpu - svpu))

### 3.3. Example

Here is an illustrate an example case per principle (1):

## 4. Constant Flow Distribution

Now let's have a look of a more complex case, the constant flow distribution operations (`updateSubscription`

&
`updateConstantFlowDistribution`

). This will solve the puzzle of how can Elon Musk sends a flow of dividends to all of his
"followers".

### 4.1. Constant Flow Formula and Its Lenses

First of all, the constant flow formula are provided through the lens abstraction, it is just a fancy way of saying some of the values of the formula are provided are a set of functions themselves:

-- ... (omitted noisy details) settledAt :: Lens' amuLs (SFT_TS sft) settledValue :: Lens' amuLs (UntappedValue (SFT_MVAL sft)) netFlowRate :: Lens' amuLs (SFT_MVAL sft) -- ... (omitted noisy details) balanceProvided (MkMonetaryUnitData a) t = let b = sv + coerce (fr * fromIntegral (t - t_s)) in -- ... (omitted noisy details) -- (.^) is the lens accessor/getter function, similar to "." in OO languages. where t_s = a^.settledAt sv = a^.settledValue fr = a^.netFlowRate

What really matters above is the formula in **b**, and knowing that it needs three set of lenses: `settledAt`

, `settledValue`

and `netFlowRate`

to be able to compute.

### 4.2. Publisher Balance Function

Per principle (2), balance function for publisher is the same as the 1 to 1 constant flow, hence its lenses are trivial:

-- ... the data record for publisher data PublisherData sft = PublisherData { pub_settled_at :: SFT_TS sft , pub_settled_value :: UntappedValue (SFT_MVAL sft) , pub_total_flow_rate :: SFT_MVAL sft } -- ... use field template to generated lenses settledAt = $(field 'pub_settled_at) settledValue = $(field 'pub_settled_value) netFlowRate = $(field 'pub_total_flow_rate)

### 4.3. Subscriber Balance Function

Balance function for subscriber is a tad more complex but still succinct. It is also provided through a set of constant flow lenses:

settledAt = readOnlyLens (\(-- ... syntaticcal pattern matching noise omitted ) -> s_t) netFlowRate = readOnlyLens (\(( -- ... syntaticcal pattern matching noise omitted ) -> if tu /= 0 then floor $ fromIntegral dcfr * u / tu else 0) settledValue = readOnlyLens (\( -- ... syntaticcal pattern matching noise omitted ) -> let compensatedΔ = dcfr * fromIntegral (t_dc - t_sc) compensatedVpuΔ = if tu /= 0 then floor $ fromIntegral compensatedΔ / tu else 0 in sv + floor (u * fromIntegral (vpu - svpu - compensatedVpuΔ)))

In addition to the common variables:

- Let
`fpu`

be flow per unit, then`dcfr`

is the distribution flow rate of the index:`dcfr = fpu * total_units`

. - In
`settledValue`

function,`t_dc`

is the`s_t`

of the publisher side, while`t_sc`

is the`s_t`

of the subscriber side.

The following visual example should show you how all these formulas compose together nicely.

### 4.4. Example

Here is an illustrate an example case per principle (1):

It should show why `compensatedVpuÎ”`

was needed behind the lens abstraction in the "bar sticks algebra" on the bottom
right side.

## 5. Inductively Covering All Cases

Now that we seem to have the basic formulas for both Instant Distribution and Constant Flow Distributions figured out, how do we know it can work for all cases?

Like many formal proofs, we need to use inductions and come up with base cases.

Using constant flow distribution as the example, there are two base cases:

- A publisher the distribute constant flow to two subscribers.
- A subscriber receives constant flow distributions from two publishers.

Along with the following laws that need to be satisfied:

- Publisher data forms a semigroup. That means it has a binary operator (for combining publisher data) and it should be associative.
- Each base case always yields zero balance in total, that means all balances sent from publisher should go to the subscribers, no more no less (apart from precision errors may rise from the actual float data type).

As a lazy engineer we sometimes do, omitting all the actual formal proof steps, the claim is that with two base cases and assuming the above laws are satisfied, then we can inductively covering all the cases of constant flow distribution agreement.

To make things even more informal, noting that we are still assuming those laws are actually satisfied. Since the specification does not use dependently typed languages such as Agda nor dependently-typed haskell, there is no way to prove the laws using types.

In the end we will need to resort to using the technique such as quickcheck^{3} for fuzzing as many cases as
possible to get higher confidence on the correctness of implementation. For example this algebraic type would allow you
to tell quickcheck to test a random combinations of all these operations and hence test the desired laws through the
properties:

-- algebraic type of all possible operations data TestOperations = Nop () | PubOp1 T_CFDAPublisherOperation | PubOp2 T_CFDAPublisherOperation | SubOp1 T_PDIDXSubscriberOperation | SubOp2 T_PDIDXSubscriberOperation deriving Show -- Testing 1 pub 2 subs scenario newtype TO_1Pub2Subs = TO_1Pub2Subs TestOperations deriving Show instance Arbitrary TO_1Pub2Subs where arbitrary = oneof [ (arbitrary :: Gen ()) <&> TO_1Pub2Subs . Nop , (arbitrary :: Gen T_CFDAPublisherOperation) <&> TO_1Pub2Subs . PubOp1 , (arbitrary :: Gen T_PDIDXSubscriberOperation) <&> TO_1Pub2Subs . SubOp1 , (arbitrary :: Gen T_PDIDXSubscriberOperation) <&> TO_1Pub2Subs . SubOp2 ] ao_1pub2subs_zero_sum_balance :: T_Timestamp -> NonEmptyList (TO_1Pub2Subs, T_Timestamp) -> Bool -- testing 2 pubs 1 sub scenario newtype TO_2Pubs1Sub = TO_2Pubs1Sub TestOperations deriving Show instance Arbitrary TO_2Pubs1Sub where arbitrary = oneof [(arbitrary :: Gen ()) <&> TO_2Pubs1Sub . Nop , (arbitrary :: Gen T_CFDAPublisherOperation) <&> TO_2Pubs1Sub . PubOp1 , (arbitrary :: Gen T_CFDAPublisherOperation) <&> TO_2Pubs1Sub . PubOp2 , (arbitrary :: Gen T_PDIDXSubscriberOperation) <&> TO_2Pubs1Sub . SubOp1 , (arbitrary :: Gen T_PDIDXSubscriberOperation) <&> TO_2Pubs1Sub . SubOp2 ] ao_2pubs1sub_zero_sum_balance :: T_Timestamp -> NonEmptyList (TO_2Pubs1Sub, T_Timestamp) -> Bool -- ... tests = describe "ConstantFlowDistributionAgreement properties" $ do it "CFDA semigroup Publisher MUD associativity" $ property semigroup_pubmud_associativity it "CFDA semigroup Publisher MUD settles pi" $ property semigroup_pubmud_settles_pi it "CFDA operations produces zero balance sum between 1 pub & 2 subs" $ property ao_1pub2subs_zero_sum_balance it "CFDA operations produces zero balance sum between 2 pubs & 1 sub" $ property ao_2pubs1sub_zero_sum_balance

## 6. What Is Next

The maths covered here form the foundation of how general distribution can work in practice, hence enabling new payment semantics that can be performed efficiently in superfluid-style payment system.

There is still much to be said about how the agreement should be structured in general, for example what does it mean that the publisher data need to have the semigroup structure? This will be explained in a future article answering the question "what makes an agreement a well behaved agreement?".

The specification of these new payment semantics will be ported to the current EVM implementation too. For both the EVM implementation and the work-in-progress Haskell specification, you can find them at: https://github.com/superfluid-finance/protocol-monorepo/.

Other Useful Links:

- Build with Superfluid, read our docs and join the conversation.
- Visit our Website or GitHub, follow us on Twitter, Discord or LinkedIn.

Article source code: https://raw.githubusercontent.com/wiki/superfluid-finance/protocol-monorepo/Presentation-denotational-payment/index.org

## Footnotes:

^{1}

Elliott, Conal. "Denotational design with type class morphisms." extended version), LambdaPix (2009).