A First-Principles-Driven Life

Posts tagged "superfluid":

27 Jan 2023

Reactive Exchanges - SLAMM dunk with Superfluid

Introduction

Superfluid protocol enables money to move between entities continuously in time with no transaction. It is a new paradigm of how the money payment system works. Using this innovative building block, one can build novel applications for payroll, subscriptions, vesting, streaming AMMs, gaming, trade finance, rentals, and NFTs. Click here to read more what is Superfluid.

Though modeling a problem domain explicitly with time is not a novel concept. In fact, functional reactive programming (FRP) that was formulated in a ICFP 97 paper1 demonstrated that we can model animations elegantly and efficiently using continuous time. More than 20 years later, it was Superfluid, the first one that successfully connected the dots between FRP and the domain of money payment system, and has made it available on more than 6 EVM (Ethereum Virtual Machine) chains2.

In this article, we focus on one of its novel applications: different designs of exchanges that can facilitate swaps continuously in time3. By now, you should understand why I shall name them "Reactive Exchanges." Reactive exchanges are types of exchanges modeled with functional reactive programming.

The article expects you to be familiar with the trading terminologies and related innovations on decentralized ledgers. Axo trade whitepaper4, for instance, provides an excellent overview of this domain. Additionally, it would be best if you had an in-depth overview of what is Superfluid is and how it works5.

Different Reactiveness

Throughout the article, we separate the "reactiveness" of an exchange into three primary functions:

  • Contribution: does the input asset enter the exchange continuously in time?
  • Swap: does swap between the input and assets happen continuously in time?
  • Distribution: is output asset distributed continuously in time?

At the end of the article, we will then compare different designs using this classification.

Pseudo Reactive Exchange

The first attempt at having reactive exchange is making only the contribution continuous in time. The actual swaps are done through an external DEX (decentralized exchange), and distribution of the swap output is done through Superfluid IDA6, both happen periodically and are triggered by keepers ("cronjob at scale").

Let's call this "pseudo reactive exchange" since the actual swaps do not continuously in time. Here is a visualization of such exchange:

pseudo-reactive-exchange.png

An example of such exchanges that is in production is Ricochet Exchange, an original and earliest example of how to build an unique exchange using Superfluid. It has been live for over an year, and provides an efficient way for anyone to DCA (dollar cost average)7 invest into on-chain assets.

Reactive Constant Function Market Maker (R-CFMM) Exchange

CFMM (Constant Function Market Maker) was the first class of AMM (Automatic Market Maker) applied to real-world financial markets4. In this article, we look into making one of the earliest and simplest versions of CFMM, Constant Liquidity Product (CLP) used in Uniswap v1 and v2 8 , 9, reactive.

To solve the equations required to make the CLP reactive, I used the python binding of the SageMath framework, a free open-source mathematics software system licensed under the GPL:

from sage.all import var, assume, function, solve

# let's define a handful of symbols
L_a, L_b, T, r, r_a, r_b, t_0, t = var("L_a", "L_b", "T", "r", "r_a", "r_b", "t_0", "t")
assume(t >= t_0)

First, let's define CLP:

from sage.all import var, assume, function, solve

def CLP(x, y, x_prime, y_prime):
    """Constant Liquidity Product Swap"""
    return x * y == x_prime * y_prime
assume(t >= t_0)

Secondly, let's try to use sage to solve the price function for selling asset A (sell amount \(a_\Delta\)) for asset B (get amount \(b_\Delta\)):

def solve_clp_a4b():
    print("# Solve CLP equation for selling A for B instantly\n")
    v_a = var("a_Δ")
    v_b = var("b_Δ")
    clp = CLP(
        L_a,
        L_b,
        L_a + v_a,
        L_b + v_b
    )
    sols = solve(clp, v_b)
    assert(len(sols) == 1)
    print(sols[0])
    print("\n")

Sage spits out the well-known equation as expected:

\[L_{b\Delta} = \frac{L_b * a_\Delta}{L_a + a_\Delta}\]

Now it comes to how to make it reactive; two functions of time need to be solved: one for asset A and another for asset B. There are not enough free variables to solve two equations, but we do know that these two equations should be elated to each other. Here was the stroke of insight, and a magic variable "q" was introduced (and please don't ask more):

def solve_rclp_rtb_bidir():
    print("# Solve Reactive CLP rtb_bidir equation\n")
    cf_a = r_a * (t - t_0)
    cf_b = r_b * (t - t_0)

    q = var("q")
    clp = CLP(
        L_a,
        L_b,
        L_a + cf_a + q * cf_b,
        L_b + cf_b + 1/q * cf_a
    )
    sols = solve(clp, q)
    print("L_{flowswap_a} =", (1/q * cf_a).subs(sols[0]))
    print("L_{flowswap_b} =", (q * cf_b).subs(sols[0]))
    print("\n")

Gratefully, Sage spits out the magic formula we are looking for. Let's call it flowswap formula:

  1. \[L_{flowswap_a} = \frac{-(r_b * t_\Delta - L_b) * r_a * t_\Delta}{r_a * t_\Delta + L_a}\]
  2. \[L_{flowswap_b} = \frac{-(r_a * t_\Delta - L_a) * r_b * t_\Delta}{r_b * t_\Delta + L_b}\]

Here is an illustration of the global view of a reactive CLP exchange:

R-CLP-global-view.png

Another way of seeing it is from how swaps look after "reactification" on the chart of the CLP formula:

R-CLP-formula-view.png

To make the exchange work for more participants, we again need to use IDA from Superfluid money, where the proportion of the flowswap output is determined by the market takers' continuous flow contributions.

Regarding "reactiveness, " market takers always "flowswap" constant flows for another non-linear flow of money, and they are both continuous in time and reactive. However, Superfluid money cannot distribute money through arbitrary formulas; that's why the distribution cannot be reactive unless a bespoke flowswap primitive is a built-in feature of the money.

You can find the work-in-progress prototype of this in the T-REX (Toy Reactive Exchange) Monorepo. If you are interested in making this closer to production, join Superfluid's wave pool program.

Zero-Intermediate-Liquidity Market Maker (ZILMM) Exchange

Another fascinating and unique variation of AMM enabled by Superfluid money is a market maker that requires zero intermediate liquidity, where liquidity goes from LPs to traders directly as constant flows. As a result, a trade-off (or feature) is that such exchanges may not easily facilitate instant swaps.

I shall call such exchange ZILMM: Zero-Intermediate-Liquidity Market Makers. The pioneer of such design is Superfluid's ecosystem project Aqueduct. We will leave the reader to discover more about the project on their own, and we will only include an illustration from them to get a taste of it:

  1. At market liquidity "equilibrium"

    aqueduct-1.png
  2. Traders tilting the "equilibrium"

    aqueduct-2.png

Since all flows involved are constant flows, it should not be a surprise that this design of the reactive exchange ticks all the reactiveness boxes!

Conclusion

Let us review the "reactiveness" of all three Superfluid money enabled market maker designs:

Exchange Type Contribution Swap Distribution Known
/ Reactiveness Reactiveness Reactiveness Reactiveness Projects
Pseudo Yes No No Ricochet
R-CFMM Yes Yes Maybe(a) T-Rex
ZILMM Yes Yes Yes Aqueduct

Note:

a) Distribution with the complex formula required by R-CFMM is viable but not necessarily desirable.

Each design has its pros and cons, and it is beyond the purpose of this article to dive into them.

However, Superfluid money demonstrably enlarged the design surface of AMM. I believe it should be a safe bet that innovations enabled by Superfluid money are not restricted to AMM and other types of financial contracts such as options, futures, interest rate swaps, etc., should have unique Superfluid money enabled designs too.

While reactive exchanges accurately reflects the underlying technology, a more playful term could be SLAMM (Streaming Liquidity Automatic Market Makers). I will end the article with a slogan:

Let's SLAMM dunk it with Superfluid.

Footnotes:

1

Elliott, Conal; Hudak, Paul. "Functional Reactive Animation". Functional Reactive Animation. ICFP ’97. Retrieve 14 July 2018.

2

All deployments of Superfluid protocol can be accessed through Superfluid app.

3

It should not to be confused with the existing financial term continuous trading.

8

Uniswap v1 Protocol Hayden Adams et al. Novembrer 2018. URL: https://docs.uniswap.org/protocol/V1/introduction. Accessed on 15/10/2021.

9

Uniswap v2 Core Hayden Adams et al. March 2020. URL: https://uniswap.org/ whitepaper.pdf. Accessed on 15/10/2021.

Tags: superfluid defi semantic money
24 Oct 2022

First Yellowpaper About Superfluid Protocol, the Beginning of Something Greater

Where Are We

We, builders of the Superfluid Protocol, have come a long way.

EVMv1 of Superfluid Protocol has been live on Polygon (then Matic Network) since a year and a half ago (May 2021). Since then, we have been live in 5 more networks, including Gnosis Chain (then xDAI Chain), Optimism, Arbitrum, Avalanche, and BNB Chain.

The significant features of the protocol are:

We have had many new product announcements, community project launches, and hackathon winners — all of which you can read about on the Superfluid medium blog.

We are fully committed to building products that expand the reach and adoption of the EVMv1 of Superfluid Protocol. For this, we invite everyone to participate in our roadmap public board, helping us shape them together.

Something Greater

First of all, the reason why we are here is that there is a central observation guiding us; consequently, we are motivated by a strong belief in how payment systems can become:

Payment systems in the information age are still modeled after their analog predecessors. We can modernize it.

Meanwhile, we are planning for an extended period of focused building for this cycle. Namely, we want to expand the depth and breadth of the idea behind the Superfluid Protocol.

More Depth

Yellowpapers & Stronger Foundation

As the first step to expand the depth of the protocol, I am happy to announce that the first yellowpaper of its series about the most fundamental part of the Superfluid idea is now available: "Denotational Semantics of General Payment Primitives, and Its Payment System."

The paper first explores the foundation of modern payment systems, which consists of a money distribution model, payment primitives, payment execution systems of financial contracts, and different forms of money mediums. Then the paper uses denotational semantics to formally define payment primitives for modern payment systems. Lastly, this paper also includes an overview of the Superfluid Protocol, a reference implementation of the payment primitives, and its payment system.

Here are some of the topics future yellowpapers will explore:

  • Composing payment primitives of modern payment systems.
  • A deterministic buffer-less modern payment execution environment.
  • A note (EUTXO) based modern payment execution environment.

These are some cross-cutting concerns of modern payment systems; they form a stronger foundation to build future Superfluid Protocol implementations.

Next Generation Architecture

Here is a sneak peek into how that next generation Superfluid Protocol implementation could look like:

superfluid-protocol-ng.png

Execution-Layer Agnostic

The architecture is deliberately execution-layer agnostic to prepare for a many-chains world.

That means deferring the decisions related to the specificity of the execution layer towards as much edge as possible, such as "dev experience overlay," "data availability," etc.

Functional Core & Data Availability

A functional core means that we apply the functional programming style to the core part of the protocol, namely (a) using denotational semantics to define payment primitives, (b) pushing data availability out of the core, (c) and composing payment primitives through combinators.

The advantages of such architecture are that:

  • It ensures we can better reason the system's security,
  • abstracting data availability so that we can try new methods such as gas-optimizing data serializations, ad-hoc merkle tree data rollups, ZK Proofs, FHE (Fully Homomorphic Encryption), etc.,
  • thinking in combinators enables powerful compositionality.

Overlay & Tooling for Dev Experience

From our experience in EVMv1, a distinct separation between core and peripherals (including dev experience overlay) should unshackle creativity in token/note interface design.

In the off-chain world, data indexers and SDKs are the critical pieces to unlock the complete development experience for the dapp developers.

Super Apps Power-Ups

Super Apps will also get power-ups from the more sound core and the better dev experience overlay, so developers should expect to build safer Super Apps easier.

Automation

Unlike EVMv1, where we added the ACL feature for automation later, the off-chain automation system will be part of the integral design of the system from day 1.

More Breadth

Superfluid Protocol EVMv2

We will still maintain our strong focus on EVM blockchains and start to work towards the EVMv2 Superfluid Protocol.

Non-EVM Prototypes

At the same time, bringing ideas behind the Superfluid Protocol everywhere is our longer-term dream. Therefore, to avoid the risk of premature favoritism, we shall not mention any particular blockchains; nonetheless, it suffices to say that a grant-seeking approach will be favored when exploring other chain implementations.

Get Involved

We’re excited to launch our yellowpaper series, and hope it helps evolve the discussion around what a modern payment system could and should look like. We have yet to publicize any research-related job posts, but if our yellowpaper series interests you and you’d like to be part of it, please visit http://jobs.superfluid.fiance or send your CV to jobs@superfluid.finance!

Tags: superfluid semantic money
18 Aug 2022

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 semantics1.

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:

  1. Publisher vpu is always updated for either a publisher operation (distributeFlow, or updateConstantFlowDistribution) or a subscriber operation (updateSubscription units).
  2. 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.
  3. 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):

ida-example1.png

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):

cfda-example1.png

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 quickcheck3 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:

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).

Tags: superfluid
Other posts
Creative Commons License
A First-Principles-Driven Life by Miao, ZhiCheng is licensed under a Creative Commons Attribution 3.0 License.