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:

  1. Verifies the input ASA transfer
  2. Reads old state (sumX, sumXSq)
  3. Computes new state from the trade
  4. Evaluates the torus invariant
  5. Checks tolerance and minOut
  6. Updates state
  7. 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+ opcode

Tolerance 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 <= TOLERANCE

Fee 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) * PRECISION

Crossing 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_int

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