Swap Verification
This page shows how the contract verifies a swap — the core operation of the protocol. We'll walk through the step-by-step logic and show the corresponding PyTeal pseudocode.
05 · Trade Execution
A swap moves the reserve point along the torus surface. The invariant is verified on-chain.
Verification Steps
For a simple swap (no tick crossings), the contract:
- Verifies the input ASA transfer
- Reads old state (sumX, sumXSq)
- Computes new state from the trade
- Evaluates the torus invariant
- Checks tolerance and minOut
- Updates state
- Emits inner transaction for output
Pseudocode
# Step 1: Verify input ASA transfer
assert gtxn[0].type == acfg.AssetTransferTx
assert gtxn[0].asset_receiver == Global.current_application_address
assert gtxn[0].xfer_asset == token_asa[token_in_index]
assert gtxn[0].amount >= amount_in
# Step 2: Read old state
sumX_old = GlobalState['sumX']
sumXSq_old = GlobalState['sumXSq']
r_int = GlobalState['rInt']
s_bound = GlobalState['sBound']
# Step 3: Compute new state
# Trade: sell amount_in of token_in, receive claimed_out of token_out
scaled_in = amount_in / AMOUNT_SCALE
scaled_out = claimed_out / AMOUNT_SCALE
sumX_new = sumX_old + scaled_in - scaled_out
# sumXSq update: (x + Δin)² - x² + (x - Δout)² - x²
# = 2x·Δin + Δin² - 2x·Δout + Δout²
x_in = reserves[token_in_index] / AMOUNT_SCALE
x_out = reserves[token_out_index] / AMOUNT_SCALE
sumXSq_new = sumXSq_old + 2 * x_in * scaled_in + scaled_in ** 2 - 2 * x_out * scaled_out + scaled_out ** 2
# Step 4: Evaluate torus invariant
# LHS = r_int²
lhs = r_int ** 2
# RHS = (α_int - r_int * √n)² + (‖w‖ - s_bound)²
alpha_int = sumX_new / sqrt(n)
norm_w_sq = sumXSq_new - (sumX_new ** 2) / n
norm_w = sqrt(norm_w_sq)
rhs = (alpha_int - r_int * sqrt(n)) ** 2 + (norm_w - s_bound) ** 2
# Step 5: Check tolerance
assert abs(lhs - rhs) <= TOLERANCE
assert claimed_out >= min_out
# Step 6: Update state
GlobalState['sumX'] = sumX_new
GlobalState['sumXSq'] = sumXSq_new
# Update reserves array
reserves[token_in_index] += amount_in
reserves[token_out_index] -= claimed_out
box_put('reserves', reserves)
# Step 7: Emit inner transaction
inner = InnerTxnBuilder.Begin()
inner.set_asset_transfer(
asset=token_asa[token_out_index],
amount=claimed_out,
receiver=Txn.sender,
close_remainder_to=Txn.sender
)
inner.submit()Key Operations
512-bit Multiplication
When computing scaled_in ** 2, the result can exceed 2⁶⁴. The contract uses mulw to get both low and high 64-bit words:
# PyTeal: (a * b) with 512-bit result
def mul512(a: Expr, b: Expr) -> Tuple[Expr, Expr]:
return (
# Low 64 bits
b * a,
# High 64 bits (via mulw)
Pop(Concat(b, a)) # mulw pushes low, high; we keep high
)Integer Square Root
The AVM's sqrt opcode computes floor(√x):
# PyTeal: integer sqrt
def isqrt(x: Expr) -> Expr:
return Sqrt(x) # TEAL 8+ opcodeTolerance Check
Due to integer division and AMOUNT_SCALE, exact equality is impossible. The contract uses:
TOLERANCE = 1000 # In scaled math space
def verify_invariant(lhs: Expr, rhs: Expr) -> Expr:
diff = If(lhs > rhs, lhs - rhs, rhs - lhs)
return diff <= TOLERANCEFee Deduction
Before verification, the contract deducts fees from the input:
fee_bps = GlobalState['fee_bps'] # e.g., 30 = 0.3%
fee_amount = (amount_in * fee_bps) / 10000
amount_in_after_fee = amount_in - fee_amount
# Fee is added to fee_growth (see fee-accounting)
fee_growth[token_in_index] += (fee_amount / r_int) * PRECISIONCrossing Verification
For swap_with_crossings, each segment includes a tickCrossedId. The contract verifies the crossing condition:
# Crossing condition: α_int normalized == k normalized
# i.e., sumX / (r_int * √n) == k / (r * √n)
def verify_crossing(
sumX: Expr,
r_int: Expr,
k_tick: Expr,
r_tick: Expr
) -> Expr:
# Cross-multiplied to avoid division:
# sumX * r * √n == k * r_int * √n
# sumX * r == k * r_int
return sumX * r_tick == k_tick * r_intIf the crossing is valid, the tick's state is flipped and the pool is re-consolidated.
Note: The actual PyTeal is more verbose due to type checking and error handling. See contract/swap.py for the full implementation.