Verified Math in ZK Circuits: Division, Exchange Rates & Overflow in Compact

If you've built smart contracts before, you probably have opinions about integer math. Solidity made you think carefully about overflow. Rust made you choose between checked_add and wrapping arithmetic. Compact — Midnight's language for ZK circuits — adds another layer of complexity, because you're not just worrying about values at runtime. You're worrying about what's provable.

This article covers the practical side of mathematical operations in Compact: why naive integer math fails in ZK proofs, how Compact's type system handles the dangerous cases, and patterns for common tasks like exchange rate calculations that look simple until they aren't.

Why Regular Integer Math Breaks in ZK Circuits

In a traditional program, integer division is simple: 7 / 2 = 3. The runtime just does it. In a ZK circuit, every operation needs to be expressed as polynomial constraints over a finite field. Division doesn't have a direct counterpart — you can't just "divide" in a constraint system.

What you can do is multiply. If you want to prove that a / b = c, you instead prove that b * c = a. This works, but it has implications:

You must prove the inverse exists. Division by zero isn't just a runtime error in ZK circuits — it's a constraint violation that makes your proof unsatisfiable. The circuit literally cannot be completed.

Remainder gets dropped. When you write 7 / 2 and the circuit computes this as integer division (c = 3), the constraint 2 * 3 = 7 is false. You need to account for the remainder explicitly: 2 * 3 + 1 = 7.

Intermediate values must stay in bounds. If you're computing inside a field of size p, intermediate multiplications can produce values larger than you expect. Compact's type system helps here, but you need to understand what it's doing.

Compact abstracts much of this, but knowing what's happening underneath makes debugging much easier.

Integer Division in Compact

Compact uses Uint<N> types — unsigned integers of exactly N bits. When you divide two Uint<N> values, you get floor division (truncation toward zero for positive numbers), and the remainder is discarded unless you explicitly capture it.

circuit divideTokens(
  witness amount: Uint<64>,
  witness shares: Uint<32>
) -> Uint<64> {
  // This is floor division — remainder is dropped
  const perShare: Uint<64> = amount / shares;
  return perShare;
}

This looks reasonable, but notice what's missing: proof that shares > 0. If shares is zero, the circuit is unsatisfiable. The prover can't generate a proof, and if you're relying on proof failure to handle errors, you've got a UX problem.

The right pattern is to assert preconditions:

circuit divideTokens(
  witness amount: Uint<64>,
  witness shares: Uint<32>
) -> Uint<64> {
  assert shares > 0 : "shares must be nonzero";
  const perShare: Uint<64> = amount / shares;
  return perShare;
}

Now the constraint is explicit. If shares = 0, the assertion fails and the circuit refuses to generate a proof. That's the correct behavior — fail loud and early rather than silently producing garbage.

When You Need the Remainder

A common pattern is distributing tokens proportionally and tracking what's left over:

circuit distributeWithRemainder(
  witness totalAmount: Uint<64>,
  witness numRecipients: Uint<32>
) -> (Uint<64>, Uint<64>) {
  assert numRecipients > 0 : "must have at least one recipient";

  const perRecipient: Uint<64> = totalAmount / numRecipients;
  const distributed: Uint<64> = perRecipient * numRecipients;
  const remainder: Uint<64> = totalAmount - distributed;

  // Sanity check: remainder must be less than numRecipients
  assert remainder < numRecipients : "remainder invariant violated";

  return (perRecipient, remainder);
}

The assertion at the end isn't strictly necessary (it follows from the arithmetic), but it's good practice. It documents your invariants and catches bugs during development if your division logic is wrong.

Exchange Rate Patterns

Exchange rates are where developers get burned most often. The problem: real exchange rates are rational numbers (1.5x, 0.333x, 2.7183x), but Compact works with integers.

The Multiply-Then-Divide Pattern

The standard approach is to scale the numerator up before dividing:

// Apply a 1.5x exchange rate: multiply by 3, divide by 2
circuit applyExchangeRate150(
  witness inputAmount: Uint<64>
) -> Uint<64> {
  assert inputAmount <= 0xFFFFFFFFFFFFFFFF / 3 : "overflow check";

  const scaled: Uint<64> = inputAmount * 3;
  const outputAmount: Uint<64> = scaled / 2;

  return outputAmount;
}

Notice the overflow check before the multiplication. inputAmount * 3 needs to fit in a Uint<64>. If inputAmount is close to 2^64 - 1, multiplying by 3 wraps around and produces garbage. The assertion ensures we catch this case.

A cleaner approach is to parameterize the rate as a numerator/denominator pair:

circuit applyRate(
  witness inputAmount: Uint<64>,
  public rateNumerator: Uint<32>,
  public rateDenominator: Uint<32>
) -> Uint<64> {
  assert rateDenominator > 0 : "denominator must be nonzero";
  assert rateNumerator > 0 : "numerator must be nonzero";

  // Overflow check: inputAmount * rateNumerator must fit in Uint<64>
  // Using 128-bit intermediate to be safe
  const intermediate: Uint<128> = (inputAmount as Uint<128>) * (rateNumerator as Uint<128>);
  const result: Uint<128> = intermediate / (rateDenominator as Uint<128>);

  // Cast back down, asserting it fits
  assert result <= 0xFFFFFFFFFFFFFFFF : "result overflow";
  return result as Uint<64>;
}

Using a wider intermediate type (Uint<128>) before casting back down is the safest approach. You don't lose precision from premature truncation, and you can explicitly check the result fits in your target type.

Fixed-Point Arithmetic

For DeFi-style contracts where you need consistent precision, fixed-point is often cleaner than ad-hoc scaling. The idea: represent all amounts with an implicit decimal point, e.g., 6 decimal places.

// Fixed-point with 6 decimal places
// 1.0 is represented as 1_000_000
// 1.5 is represented as 1_500_000

const DECIMALS: Uint<32> = 1_000_000;

circuit multiplyFixedPoint(
  witness a: Uint<64>,   // fixed-point value
  witness b: Uint<64>    // fixed-point value
) -> Uint<64> {
  // a and b are both scaled by DECIMALS
  // their product is scaled by DECIMALS^2
  // we need to divide by DECIMALS once to get back to DECIMALS scale
  const product: Uint<128> = (a as Uint<128>) * (b as Uint<128>);
  const scaled: Uint<128> = product / (DECIMALS as Uint<128>);

  assert scaled <= 0xFFFFFFFFFFFFFFFF : "fixed-point overflow";
  return scaled as Uint<64>;
}

The tricky part is always: who scales what. Document your invariants. If a function expects its input in fixed-point, say so. If it returns raw integers, say that too. Mixing scaled and unscaled values is a silent bug.

Overflow Protection

Uint<N> Type Bounds

The Uint<N> type in Compact is a hard constraint — values must fit in exactly N bits. Overflow is a circuit constraint violation, not a runtime exception. The prover will refuse to generate a proof if a value exceeds its type bound.

This is actually safer than many languages. In Solidity pre-0.8, uint256 overflow silently wrapped. In Compact, overflow makes the proof fail loudly.

But "loud" doesn't mean "helpful." If your circuit fails to prove because of an unexpected overflow, you need to trace back which constraint failed. Good practice: add assertions before any operation that could overflow.

circuit safeMultiply(
  witness a: Uint<64>,
  witness b: Uint<64>
) -> Uint<64> {
  // Before multiplying, check the result fits
  // If b != 0: a must be <= MAX_U64 / b
  if b != 0 {
    assert a <= 0xFFFFFFFFFFFFFFFF / b : "multiplication would overflow";
  }

  return a * b;
}

Choosing the Right Bit Width

One common mistake: using Uint<64> for everything. Wider types mean larger circuits and bigger proofs. Use the smallest type that safely holds your values.

// BAD: Using Uint<256> for a value that's always 0-100
circuit badPercentage(witness pct: Uint<256>) -> Uint<256> {
  assert pct <= 100 : "percentage must be 0-100";
  return pct;
}

// GOOD: Use Uint<7> (max value 127, fits 0-100)
circuit goodPercentage(witness pct: Uint<7>) -> Uint<7> {
  assert pct <= 100 : "percentage must be 0-100";
  return pct;
}

The circuit for goodPercentage will have fewer constraints, generate faster, and produce smaller proofs.

Checked vs. Unchecked Arithmetic

Compact doesn't have explicit "unchecked" blocks like Rust or Solidity 0.8+. All arithmetic operates within the type's bit width. If you want wrapping behavior (rare in ZK contracts, but occasionally useful for hash functions), you need to implement it explicitly using modular arithmetic.

Common Pitfalls

Pitfall 1: Ordering Matters for Truncation

// These produce different results!
const result1: Uint<64> = (amount * 2) / 3;  // Multiplies first, then divides
const result2: Uint<64> = amount / 3 * 2;    // Divides first (loses precision), then multiplies

For a value like amount = 10:

• result1 = (10 * 2) / 3 = 20 / 3 = 6
• result2 = (10 / 3) * 2 = 3 * 2 = 6 (same here)

For amount = 11:

• result1 = (11 * 2) / 3 = 22 / 3 = 7
• result2 = (11 / 3) * 2 = 3 * 2 = 6 ← different!

Always multiply before dividing unless you have a specific reason not to.

Pitfall 2: Silent Loss of Precision in Intermediate Results

// Calculating 10% of a value
// BAD: loses up to 9 tokens of precision
const tenPercent: Uint<64> = amount / 10;

// BETTER: more precise (loses up to 0 if amount is divisible by 10)
const tenPercent: Uint<64> = (amount * 10) / 100;  // Same thing, same precision

// BEST for financial contexts: capture and handle the remainder
const tenPercentFloor: Uint<64> = amount / 10;
const remainder: Uint<64> = amount - (tenPercentFloor * 10);
// Now route remainder somewhere (return to user, burn it, whatever your protocol decides)

Pitfall 3: Forgetting That Division Changes Type Behavior

When you divide Uint<64> by Uint<64>, the result is Uint<64>. The result can be zero. Downstream code that doesn't handle zero will have bugs:

circuit badSharePrice(
  witness totalValue: Uint<64>,
  witness numShares: Uint<64>
) -> Uint<64> {
  const pricePerShare: Uint<64> = totalValue / numShares;
  // If numShares > totalValue, pricePerShare = 0
  // If someone buys using this price, they pay 0 — free shares
  return pricePerShare;
}

Any protocol that uses a computed price should handle the zero case explicitly.

Putting It Together: A Token Swap Circuit

Here's a more complete example — a simple constant-product AMM swap that handles the math carefully:

contract TokenSwap {
  ledger reserveA: Uint<128>;
  ledger reserveB: Uint<128>;

  // Swap exact input amount of token A for token B
  // Uses constant product formula: (reserveA + amountIn) * (reserveB - amountOut) = k
  circuit swapAForB(
    witness amountIn: Uint<64>,
    public minAmountOut: Uint<64>
  ) -> Uint<64> {
    assert amountIn > 0 : "amountIn must be positive";
    assert reserveA > 0 : "reserveA must be nonzero";
    assert reserveB > 0 : "reserveB must be nonzero";

    // Apply 0.3% fee: amountIn * 997 / 1000
    // Overflow check: amountIn * 997 must fit in Uint<128>
    const amountInWithFee: Uint<128> = (amountIn as Uint<128>) * 997;

    // Calculate output: amountOut = reserveB * amountInWithFee / (reserveA * 1000 + amountInWithFee)
    const numerator: Uint<128> = reserveB * amountInWithFee;
    const denominator: Uint<128> = reserveA * 1000 + amountInWithFee;

    assert denominator > 0 : "denominator must be nonzero";

    const amountOut: Uint<128> = numerator / denominator;

    // Downcast safely
    assert amountOut <= 0xFFFFFFFFFFFFFFFF : "amountOut overflow";
    const amountOutU64: Uint<64> = amountOut as Uint<64>;

    // Slippage check
    assert amountOutU64 >= minAmountOut : "slippage too high";

    return amountOutU64;
  }
}

Notice how Uint<128> is used for intermediate calculations to avoid overflow, and the result is only cast back to Uint<64> after an explicit bounds check.

Summary

Mathematical operations in Compact are safer than many languages because type violations fail at proof generation, not silently. But that safety requires you to:

1. Always check for division by zero with explicit assertions
2. Multiply before dividing to preserve precision
3. Use wider intermediate types for operations that might overflow
4. Capture remainders when your protocol needs precise accounting
5. Use the smallest types that fit to keep circuit size small
6. Document your fixed-point conventions when using scaled integers

The ZK proving system is fundamentally more strict than a traditional runtime — it won't let you ignore a constraint violation. That strictness is your friend if you work with it rather than against it.