The blockchain world has been shaken by the arrival of Decentralized Finance (DeFi), a movement aiming to recreate traditional financial systems using decentralized technologies. This means open, transparent, and permissionless access to financial products and services, without relying on centralized institutions.
Key Innovation: Automated Market Makers (AMMs)
One of the core innovations within DeFi is AMMs, which have played a crucial role in the growth of decentralized exchanges (DEXs). These smart contracts facilitate token exchange on a blockchain, providing both liquidity and price discovery for different assets.
Understanding AMMs
Unlike traditional order book-based exchanges, AMMs don't rely on matching buyers and sellers directly. Instead, they use mathematical formulas to automatically determine prices and execute trades. This approach offers several advantages, including:
Transparency: Open-source nature allows anyone to inspect the code and verify operations.
Accessibility: Anyone with an internet connection and a compatible wallet can participate.
User-friendliness: Eliminates the need for order books, simplifying trading.
Constant Sum AMMs: A Popular Choice
A specific type of AMM, called Constant Sum AMMs, maintains a constant sum of assets within a trading pair. This is achieved through the formula:
x * y = k
where:
x and y represent the quantities of two tokens in a liquidity pool.
k is a constant, ensuring the sum of tokens remains the same even after trades.
The most famous example is Uniswap V2, utilizing this formula to adjust token prices based on supply and demand within the pool.
Deep Dive into Constant Sum AMMs
Let's explore the inner workings and importance of these AMMs:
Initialization:
Liquidity providers deposit two tokens in equal value (e.g., ETH and DAI) into a smart contract representing the pool.
Price Calculation:
The initial price of Token A in terms of Token B is calculated using the constant sum formula.
Trading:
Based on current balances, the price adjusts when users trade:
Buying Token A increases its price and decreases Token B's price.
Selling Token A decreases its price and increases Token B's price.
The amount of tokens received depends on the price change and the constant sum property.
Arbitrage Opportunities:
Price differences between AMM and market price create arbitrage opportunities, allowing traders to profit by buying low and selling high.
Liquidity Provision:
Liquidity providers earn fees proportional to their contribution, making it an attractive way to earn passive income.
Benefits of Constant Sum AMMs
These AMMs offer several advantages that have fueled their popularity in DeFi:
Efficient Liquidity Provision: Encourage adding funds to pools, ensuring liquidity for traders.
User-Friendly Interface: Simplify trading by removing order books and automatic matching.
Transparency and Accessibility: Provide open-source code and access to anyone with internet connectivity.
Implementing a Constant Sum AMM
For the technically inclined, we can explore implementing a simple Constant Sum AMM using Solidity, Ethereum's smart contract programming language. This would involve creating a basic AMM for trading two tokens, simulating the concepts discussed above.
This markdown format provides a structured and readable way to present the information about DeFi and AMMs. Additionally, the use of headers and code blocks enhances clarity and organization.
Properties and Invariants of the AMM1 Contract:
Here some examples to check the AMM properties and invariants:
Global Properties:
Invariant:total = balanceA + balanceB holds at all times. This ensures the constant sum property of the AMM.
Invariant: price and balance behaviour hold their proportions all the times due to the constant product formula.
Function Properties:
initialize:
Only the owner can call it.
It can only be called once.
Both initialA and initialB must be greater than zero.
price:
Returns a non-zero value.
tradeAToB:
amountA must be greater than zero.
The contract must have enough balanceA to fulfill the trade.
The price of Token A after the trade is not the same as before (constant product formula).
tradeBToA:
amountB must be greater than zero.
The contract must have enough balanceB to fulfill the trade.
The price of Token B after the trade is not the same as before (constant product formula).
addLiquidity:
Both amountA and amountB must be greater than zero.
The total liquidity increases by the sum of added tokens.
removeLiquidity:
amount must be greater than zero and less than or equal to the total liquidity.
The share of tokens removed is proportional to the total liquidity.
The total liquidity decreases by the removed amount.
Additional Notes:
The contract does not handle potential overflow/underflow issues during calculations.
The code does not implement any access control for functions other than initialize.
The contract does not include any rebalancing mechanism to maintain a specific price ratio.
Formal Verification Considerations:
Formal verification tools can be used to rigorously check if the code adheres to the stated properties and invariants.
The chosen formal verification method should be able to handle complex mathematical relationships within the smart contract.
It is crucial to consider all potential edge cases and corner scenarios during the verification process.
Disclaimer:
Adding Liquidity
The process of adding liquidity to an Automated Market Maker (AMM) that follows a constant product model, such as Uniswap or SushiSwap. This model is based on the principle that the product of the amounts of two assets (x and y) in the pool remains constant, denoted by k. When liquidity is added, the amounts of these assets change, but their product remains constant. Let's break down the steps:
Initial State: The initial state of the pool is represented by xy = k, where x and y are the amounts of two assets in the pool, and k is a constant that represents the product of these amounts.
Adding Liquidity: When liquidity is added, the amounts of both assets change slightly. Let's denote the small changes in the amounts of the two assets as dx and dy. After adding liquidity, the new amounts of the assets are x + dx and y + dy , and the new product of these amounts is k.
No Price Ratio Change: The formula (x + dx)(y + dy) = k represents the new product of the amounts after adding liquidity. The goal is to find how dy changes relative to dx to maintain the price ratio between the two assets unchanged, i.e., x / y = (x + dx) / (y + dy).
Equating the Ratios: To ensure the price ratio remains unchanged, we equate the ratios of the amounts before and after adding liquidity:
x / y = (x + dx) / (y + dy) . This leads to the equation:
x(y + dy) = y(x + dx)
Solving for dy: By isolating dy on one side of the equation, we get x * dy = y * dx. This equation shows that the change in the amount of asset y * dy is proportional to the change in the amount of asset x * dx, with the proportionality constant being the ratio of y and x.
Deriving dy: Finally, solving for dy gives us dy = y / x * dx. This formula tells us how much of asset y needs to be added (or removed) to maintain the price ratio between the two assets unchanged when adding (or removing) a certain amount of asset x.
In summary, this formula is crucial for understanding how liquidity is added to an AMM without changing the price ratio between the two assets. It ensures that the market remains fair and that users receive the expected returns on their liquidity provision.
xy = k
(x + dx)(y + dy) = k'
No price change, before and after adding liquidity
x / y = (x + dx) / (y + dy)
x(y + dy) = y(x + dx)
x * dy = y * dx
x / y = dx / dy
dy = y / x * dx
Miniting Shares
How to calculate the number of shares to mint when adding liquidity to a constant product Automated Market Maker (AMM) ? The formula is based on the concept of liquidity and the proportion of the total liquidity that the new liquidity contributes. Here's a breakdown of the key components and the formula:
Key Components:
f(x, y): The value of liquidity, defined as the square root of the product of the amounts of two tokens (x and y).
L0: The initial value of liquidity before adding new liquidity.
L1: The value of liquidity after adding new liquidity (dx and dy).
T: The total number of shares.
s: The number of shares to mint.
Formula:
The formula is derived from the proportional increase in liquidity and the corresponding increase in shares. The goal is to ensure that the total shares increase proportionally to the increase in liquidity.
Initial Liquidity (L0): The initial liquidity is calculated as sqrt(xy), where x and y are the amounts of the two tokens.
New Liquidity (L1): After adding new liquidity (dx and dy), the new liquidity is calculated as sqrt((x + dx) * (y + dy)).
Proportional Increase in Shares: The formula ensures that the total shares increase proportionally to the increase in liquidity. This is represented as L1 / L0 = (T + s) / T, where s is the number of shares to mint.
Calculating Shares (s): To find the number of shares to mint (s), the formula rearranges the proportional increase equation to solve for s: (L1 - L0) * T / L0 = s.
Implementation in Code:
In the provided Solidity code, the formula is implemented in the addLiquidity function. If the total supply of shares (totalSupply) is zero, it means the pool is empty, and the shares to mint are calculated directly as the square root of the product of the amounts of the two tokens. Otherwise, the shares to mint are calculated as the minimum of two expressions:
(amount0 * totalSupply) / reserve0
(amount1 * totalSupply) / reserve1
This ensures that the shares minted are proportional to the amounts of the two tokens added and the current reserves of these tokens in the pool. The require(shares > 0, "shares = 0"); line ensures that at least one share is minted, preventing division by zero or other potential issues.
Conclusion:
The formula and its implementation in the code ensure that the addition of liquidity to the AMM results in a proportional increase in shares, maintaining the constant product formula's invariant. This mechanism allows liquidity providers to earn fees based on their share of the total liquidity in the pool.
f(x, y) = value of liquidity
We will define f(x, y) = sqrt(xy)
L0 = f(x, y)
L1 = f(x + dx, y + dy)
T = total shares
s = shares to mint
Total shares should increase proportional to increase in liquidity
L1 / L0 = (T + s) / T
L1 * T = L0 * (T + s)
(L1 - L0) * T / L0 = s
Removing Liquidity
The burn formula in the Automated Market Maker (AMM) protocol is designed to calculate the amount of liquidity to remove from the pool when a user decides to withdraw their liquidity shares. This process is crucial for maintaining the invariant of the constant product formula in AMMs, which ensures that the product of the reserves of the two tokens in the pool remains constant.
Here's a breakdown of the burn formula and its components:
Initial Variables:
s: The number of shares the user wants to burn.
T: The total supply of shares in the pool.
x: The amount of token0 in the pool.
y: The amount of token1 in the pool.
Calculating Amounts to Remove (dx, dy):
The goal is to find dx and dy such that the invariant v / L = s / T holds, where v is the volume of the liquidity being removed, L is the total liquidity in the pool, and s is the shares being burned.
The volume v is calculated as the square root of the product of dx and dy (sqrt(dxdy)).
The total liquidity L is the square root of the product of x and y (sqrt(xy)).
Invariant Equation:
The invariant equation is v / L = s / T.
Substituting the expressions for v and L gives sqrt(dxdy) / sqrt(xy) = s / T.
Solving for dx and dy:
To maintain the price ratio x / y constant, it's required that dx / dy = x / y.
Substituting dy = dx * y / x into the invariant equation simplifies it to sqrt(dx * dx * y / x) = s / T.
Solving for dx gives dx = s / T * sqrt(xy) / sqrt(y / x) = s / T * x.
Solving for dy gives dy = s / T * y.
Burning Shares:
The burn function is called with the number of shares to be burned (_shares).
This function reduces the user's balance of shares and the total supply of shares in the pool.
Adjusting Reserves:
After burning the shares, the reserves of token0 and token1 in the pool are adjusted by subtracting the amounts of liquidity removed (amount0 and amount1).
The tokens are then transferred back to the user.
This burn formula ensures that the user can withdraw their liquidity shares proportionally to their share of the total pool, maintaining the invariant of the constant product formula. This is crucial for the stability and functionality of the AMM, allowing users to withdraw their funds without significantly impacting the pool's liquidity or the price ratio of the tokens.
dx, dy = amount of liquidity to remove
dx = s / T * x
dy = s / T * y
Proof
Let's find dx, dy such that
v / L = s / T
where
v = f(dx, dy) = sqrt(dxdy)
L = total liquidity = sqrt(xy)
s = shares
T = total supply
--- Equation 1 ---
v = s / T * L
sqrt(dxdy) = s / T * sqrt(xy)
Amount of liquidity to remove must not change price so
dx / dy = x / y
replace dy = dx * y / x
sqrt(dxdy) = sqrt(dx * dx * y / x) = dx * sqrt(y / x)
Divide both sides of Equation 1 with sqrt(y / x)
dx = s / T * sqrt(xy) / sqrt(y / x)
= s / T * sqrt(x^2) = s / T * x
Likewise
dy = s / T * y
Introduction to DeFi and AMMs
DeFi: A Revolution in Finance
The blockchain world has been shaken by the arrival of Decentralized Finance (DeFi), a movement aiming to recreate traditional financial systems using decentralized technologies. This means open, transparent, and permissionless access to financial products and services, without relying on centralized institutions.
Key Innovation: Automated Market Makers (AMMs)
One of the core innovations within DeFi is AMMs, which have played a crucial role in the growth of decentralized exchanges (DEXs). These smart contracts facilitate token exchange on a blockchain, providing both liquidity and price discovery for different assets.
Understanding AMMs
Unlike traditional order book-based exchanges, AMMs don't rely on matching buyers and sellers directly. Instead, they use mathematical formulas to automatically determine prices and execute trades. This approach offers several advantages, including:
Constant Sum AMMs: A Popular Choice
A specific type of AMM, called Constant Sum AMMs, maintains a constant sum of assets within a trading pair. This is achieved through the formula:
where:
xandyrepresent the quantities of two tokens in a liquidity pool.kis a constant, ensuring the sum of tokens remains the same even after trades.The most famous example is Uniswap V2, utilizing this formula to adjust token prices based on supply and demand within the pool.
Deep Dive into Constant Sum AMMs
Let's explore the inner workings and importance of these AMMs:
Initialization:
Price Calculation:
Trading:
Arbitrage Opportunities:
Liquidity Provision:
Benefits of Constant Sum AMMs
These AMMs offer several advantages that have fueled their popularity in DeFi:
Implementing a Constant Sum AMM
For the technically inclined, we can explore implementing a simple Constant Sum AMM using Solidity, Ethereum's smart contract programming language. This would involve creating a basic AMM for trading two tokens, simulating the concepts discussed above.
This markdown format provides a structured and readable way to present the information about DeFi and AMMs. Additionally, the use of headers and code blocks enhances clarity and organization.
Properties and Invariants of the AMM1 Contract:
Here some examples to check the AMM properties and invariants:
Global Properties:
total = balanceA + balanceBholds at all times. This ensures the constant sum property of the AMM.Function Properties:
initialize:initialAandinitialBmust be greater than zero.price:tradeAToB:amountAmust be greater than zero.tradeBToA:amountBmust be greater than zero.addLiquidity:amountAandamountBmust be greater than zero.removeLiquidity:amountmust be greater than zero and less than or equal to the total liquidity.Additional Notes:
initialize.Formal Verification Considerations:
Disclaimer:
Adding Liquidity
The process of adding liquidity to an Automated Market Maker (AMM) that follows a constant product model, such as Uniswap or SushiSwap. This model is based on the principle that the product of the amounts of two assets (x and y) in the pool remains constant, denoted by
k. When liquidity is added, the amounts of these assets change, but their product remains constant. Let's break down the steps:Initial State: The initial state of the pool is represented by
xy = k, wherexandyare the amounts of two assets in the pool, andkis a constant that represents the product of these amounts.Adding Liquidity: When liquidity is added, the amounts of both assets change slightly. Let's denote the small changes in the amounts of the two assets as
dxanddy. After adding liquidity, the new amounts of the assets arex + dxandy + dy, and the new product of these amounts isk.No Price Ratio Change: The formula
(x + dx)(y + dy) = krepresents the new product of the amounts after adding liquidity. The goal is to find howdychanges relative todxto maintain the price ratio between the two assets unchanged, i.e.,x / y = (x + dx) / (y + dy).Equating the Ratios: To ensure the price ratio remains unchanged, we equate the ratios of the amounts before and after adding liquidity:
x / y = (x + dx) / (y + dy). This leads to the equation:x(y + dy) = y(x + dx)Solving for
dy: By isolatingdyon one side of the equation, we getx * dy = y * dx. This equation shows that the change in the amount of assety * dyis proportional to the change in the amount of assetx * dx, with the proportionality constant being the ratio ofyandx.Deriving
dy: Finally, solving fordygives usdy = y / x * dx. This formula tells us how much of assetyneeds to be added (or removed) to maintain the price ratio between the two assets unchanged when adding (or removing) a certain amount of assetx.In summary, this formula is crucial for understanding how liquidity is added to an AMM without changing the price ratio between the two assets. It ensures that the market remains fair and that users receive the expected returns on their liquidity provision.
Miniting Shares
How to calculate the number of shares to mint when adding liquidity to a constant product Automated Market Maker (AMM) ? The formula is based on the concept of liquidity and the proportion of the total liquidity that the new liquidity contributes. Here's a breakdown of the key components and the formula:
Key Components:
Formula:
The formula is derived from the proportional increase in liquidity and the corresponding increase in shares. The goal is to ensure that the total shares increase proportionally to the increase in liquidity.
Initial Liquidity (L0): The initial liquidity is calculated as
sqrt(xy), wherexandyare the amounts of the two tokens.New Liquidity (L1): After adding new liquidity (dx and dy), the new liquidity is calculated as
sqrt((x + dx) * (y + dy)).Proportional Increase in Shares: The formula ensures that the total shares increase proportionally to the increase in liquidity. This is represented as
L1 / L0 = (T + s) / T, wheresis the number of shares to mint.Calculating Shares (s): To find the number of shares to mint (
s), the formula rearranges the proportional increase equation to solve fors:(L1 - L0) * T / L0 = s.Implementation in Code:
In the provided Solidity code, the formula is implemented in the
addLiquidityfunction. If the total supply of shares (totalSupply) is zero, it means the pool is empty, and the shares to mint are calculated directly as the square root of the product of the amounts of the two tokens. Otherwise, the shares to mint are calculated as the minimum of two expressions:(amount0 * totalSupply) / reserve0(amount1 * totalSupply) / reserve1This ensures that the shares minted are proportional to the amounts of the two tokens added and the current reserves of these tokens in the pool. The
require(shares > 0, "shares = 0");line ensures that at least one share is minted, preventing division by zero or other potential issues.Conclusion:
The formula and its implementation in the code ensure that the addition of liquidity to the AMM results in a proportional increase in shares, maintaining the constant product formula's invariant. This mechanism allows liquidity providers to earn fees based on their share of the total liquidity in the pool.
Removing Liquidity
The burn formula in the Automated Market Maker (AMM) protocol is designed to calculate the amount of liquidity to remove from the pool when a user decides to withdraw their liquidity shares. This process is crucial for maintaining the invariant of the constant product formula in AMMs, which ensures that the product of the reserves of the two tokens in the pool remains constant.
Here's a breakdown of the burn formula and its components:
Initial Variables:
s: The number of shares the user wants to burn.T: The total supply of shares in the pool.x: The amount of token0 in the pool.y: The amount of token1 in the pool.Calculating Amounts to Remove (
dx,dy):dxanddysuch that the invariantv / L = s / Tholds, wherevis the volume of the liquidity being removed,Lis the total liquidity in the pool, andsis the shares being burned.vis calculated as the square root of the product ofdxanddy(sqrt(dxdy)).Lis the square root of the product ofxandy(sqrt(xy)).Invariant Equation:
v / L = s / T.vandLgivessqrt(dxdy) / sqrt(xy) = s / T.Solving for
dxanddy:x / yconstant, it's required thatdx / dy = x / y.dy = dx * y / xinto the invariant equation simplifies it tosqrt(dx * dx * y / x) = s / T.dxgivesdx = s / T * sqrt(xy) / sqrt(y / x) = s / T * x.dygivesdy = s / T * y.Burning Shares:
burnfunction is called with the number of shares to be burned (_shares).Adjusting Reserves:
token0andtoken1in the pool are adjusted by subtracting the amounts of liquidity removed (amount0andamount1).This burn formula ensures that the user can withdraw their liquidity shares proportionally to their share of the total pool, maintaining the invariant of the constant product formula. This is crucial for the stability and functionality of the AMM, allowing users to withdraw their funds without significantly impacting the pool's liquidity or the price ratio of the tokens.