gnosis / dex-zksnarks

Code to generate snark proofs for batch auction result validation of the Gnosis d.exchange
46 stars 7 forks source link

Representation of prices/volumes and surplus #14

Open fleupold opened 5 years ago

fleupold commented 5 years ago

In order to verify batch auction results, we need to represent market prices, limit prices and volumes as field elements and use arithmetic operations to calculate things like trader surplus and updated account balances.

In particular the operations we have to support are:

  1. Compare limit against market price (to decide if order is touched)
  2. Given volume and market price, calculate buyVolume
  3. Given volume, market price and limit, calculate traderSurplus
  4. Given market price and volume, update balances

Proposal:

Assuming we have a type Decimal that can be represented in n bits. Lets moreover assume types for referring to Tokens as well as Accounts exist.

We can model an order as

struct Order {
  Account accountId;
  Token fromToken;
  Token toToken;
  Decimal sellAmount;
  Decimal buyAmount;
};

And a price as

struct Price {
  Decimal fromAmount;
  Decimal toAmount;
};

Prices would be provided as private input (bit-vector of 2*n*#tokens), where the fromAmount of the i-th item is denoted in Token_i, and toAmount is always denoted in a reference token (e.g. Token_0).

Let price(A->B) denote the price from token with index A to token with index B (e.g. price(GNO->RDN) = 10 means for 1 GNO we receive 10 RDN). Note, that we can easily invert a price (that is given price(A->B), compute price(B->A)) by swapping fromAmount and toAmount

Let's take a look at the operations we need to support:

  1. Compare limit against market price (to decide if order is touched)
    bool isTouched(Order o, Price marketPrices[TOKENS]) {
    // returns true iff limit(o.fromToken -> o.toToken) >= market(o.fromToken -> o.toToken)
    // o.buyAmount/o.sellAmount >= prices[o.fromToken] / prices[o.toToken]
    // o.buyAmount/o.sellAmount >= (prices[o.fromToken].toAmount/prices[o.fromToken].fromAmount) / (prices[o.toToken].toAmount/prices[o.toToken].fromAmount)
    // o.buyAmount/o.sellAmount >= (prices[o.fromToken].toAmount/prices[o.fromToken].fromAmount) * (prices[o.toToken].fromAmount/prices[o.toToken].toAmount)
    // multiplied out to avoid division, which is not defined in finite field
    return o.buyAmount * prices[o.toToken].toAmount * prices[o.fromToken].fromAmount >= prices[o.fromToken].toAmount * prices[o.toToken].fromAmount * o.sellAmount
    }

Note, that this requires three multiplications, and thus limits the size of Decimal to be less than 84 bits. If it was 85 and we would be multiplying the largest possible values together, that is (2**85 -1)**3) > p we would overflow the finite field.

  1. Given volume and market price, calculate buyVolume

Assuming the volume is given as a vector of Decimal triples (one triplet per order)

struct Volume {
  Decimal sellVolume;
  Decimal buyVolume;
  Decimal surplus;
};

In order to verify that the Volume is valid, we need to make sure it has the same ratio as the market price.

bool verifyVolume(Order o, Volume v, Price marketPrices[TOKENS]) {
  // similar process as above
  // v.buyVolume/v.sellVolume == prices[o.fromToken] / prices[o.toToken]
  return v.buyVolume * prices[o.toToken].toAmount * prices[o.fromToken].fromAmount == prices[o.fromToken].toAmount * prices[o.toToken].fromAmount * v.sellVolume
}

Then calculating the buy and sell volume becomes just accessing the respective field on the Volume struct:

field buyVolume(Volume v) {
  return v.buyVolume
}
field sellVolume(Volume v) {
  return v.sellVolume
}
  1. Given volume, market price and limit, calculate traderSurplus

Trader surplus for a single order can be defined as (limitPrice - marketPrice) * sellVolume . Since surplus is part of the Volume struct, we can simply add it together. However we have to check that it was calculated correctly. In fact we can reuse the formula from 1) and check that the limit is respected and the surplus is correct in one step by making it an equality check.

bool verifySurplus(Order o, Volume v, Price marketPrices[TOKENS]) {
  // limit(A->B)*sellVolume == surplus + marketPrice(A->B)*sellVolume
  return v.sellVolume * o.buyAmount * prices[o.toToken].toAmount * prices[o.fromToken].fromAmount == surplus + prices[o.fromToken].toAmount * prices[o.toToken].fromAmount * o.sellAmount * v.sellVolume
}

Here we are doing 4 multiplications, thus limiting our size for Decimal to 63bit.

  1. Given market price and volume, update balances

Since volumes are modelled as both sell- as well as buyVolume adjusting the balance becomes trivial:

void updateBalance(Order o, Volume v, field balances[ACCOUNTS][TOKENS]) {
  balances[order.accountId][order.fromToken] -= v.sellVolume;
  balances[order.accountId][order.toToken] += v.buyVolume;
}
fleupold commented 5 years ago

Some disadvantages of fractional encoding:

In terms of on-chain cost:

Since we expect to have more volumes than tokens, the solution using rationals should be cheaper in terms of on-chain cost.

fleupold commented 5 years ago

Another way to potentially model prices, volumes and balances is using some form of floating point notation. We could define

struct Float {
  field254 mantissa; //e.g. 60 bits
  field254 exponent; // e.g. 4 bits

  Float add(Float other) {
    // check for overflow and potentially shift numbers to make mantissa small enough to not overflow
    field254 difference = exponent - other.exponent
    if (difference > 0) {
      return { mantissa + (other.mantissa * difference), exponent };
    } else {
     return { (mantissa * exponent) + other.mantissa, other.exponent };
    }
  }

  Float multiply(Float other) {
    // check for overflow and potentially shift numbers to make mantissa small enough to not overflow
    return { mantissa * other.mantissa, exponent + other.exponent};
  }
}

However this would potentially make the arithmetic operations really expensive in terms of constraints (using if checks, inequalities, loops etc.) and might be something to explore later (not for an initial implementation of the snark).

josojo commented 5 years ago

Okay,

here I am trying to formulate my original model. Not sure, how good it is:

Proposal:

We have most of the variables as (amount of tokens held by an account, amount in the order) type 'Decimal' that can be represented in n bits. Another type is 'Fraction', it represents the variable price with 2m bits, where 2**(m+1) represents the one. The fractional fulfillment of the orders is described by m bits, as this only needs to represent numbers between 0 and 1. The data type, we want to call: 'Fractional'.

We can model an order as

struct Order {
  Account accountId;
  Token fromToken;
  Token toToken;
  Decimal sellVolume;
  Fraction price;
};

And a price as

Fraction price;

Prices would be provided as private input (bit-vector of 2*m*#tokens). All prices are given with respect to one reference token.

Let price(A->B) denote the price from token with index A to token with index B

Note, that we cannot easily invert a price. We would need to check the inverse prices provided by private input by

bool isInvers(Fraction price(A->B), Fraction price(B->A)) {
prod = price(A->B)*price(B->A)>>m
one =  2**(m+1) 
 return prod - one<= 0 && one - prod <= 1
}

The function >>m will just cut of the last m digits, which are just representing fractional amounts. The substration 'prod - one' is a bitwise subtraction and not a subtraction in the underlying field. The result of a bitwise substraction cannot be smaller than 0. The inequality one - prod <= 1 is checked by requiring all bits to be equal to 0, besides the last one. Note that we are not checking that prod - one<= 1, but prod - one<= 0. This enforces that the opposite price is rounded down

Let's take a look at the operations we need to support:

  1. Compare limit against market price (to decide if order is touched)
    bool isTouched(Order o, Fraction marketP[TOKENS]) {
    returns true iff limit(o.fromToken -> o.toToken) >= marketP(o.fromToken -> o.toToken)
    //this would be a bitwise >= operation 
    }

Note, that this requires 2m circuits

  1. Given volume and market price, calculate buyVolume

Assuming the volume is given as a vector of fractional fulfillments

struct Volume {
  Fractional fractionFulfillment;
};

We can calculate the final buy and sellvolumes with these numbers.

void  calcVolume(Order o, Fraction priceFraction(buyToken->SellToken), Fractional fractionFulfillment) {
  // verify order volume
 sellVolume = order.Volume * fractionFulfillment>>m
 buyVolume = order.Volume * priceFraction * fractionFulfillment>>2m
}
  1. Given volume, market price and limit, calculate traderSurplus

Trader surplus for a single order can be defined as (limitPrice - marketPrice) * sellVolume *conversionIntoReferenceVolume .

Decimal calcSurplus(Order o, Decimal sellvolume, Fractional marketPrices[TOKENS]) {
  // limit(A->B)*sellVolume == surplus + marketPrice(A->B)*sellVolume
  return (priceMarket - o.priceOrder)* sellvolume) * marketPrices(o.token -> referenceToken)>>2m

// multiplying bits estimate 2m+n+2m
  1. Given market price and volume, update balances

Since volumes are modelled as both sell- as well as buyVolume adjusting the balance becomes trivial:

void updateBalance(Order o, Volume v, field balances[ACCOUNTS][TOKENS]) {
  balances[order.accountId][order.fromToken] -= v.sellVolume;
  balances[order.accountId][order.toToken] += v.buyVolume;
}
  1. Calculate constraints

Also, the volume constraints need to be checked at the end of the calculation

void checkVolumes(Token token1) {
  for all token
         sellvolumes =sum(v.sellVolume(token->token1);
         buyvolumes =sum(v.buylVolume(token1->token);

return sellvolumes  - buyvolumes <=1 &&  buyvolumes - sellvolumes   <=1
}

Regarding Overflows: The biggest multiplication is done in verifySurplus with 2m+n+2m bits. That means 4m+n < 254

Regarding accurancy lost: price are introducing an error of 2*(-m). -> volumes, generate might get an error of 1 -> (priceMarket - priceOrder) volume* conversionPrice)>>2m

All over the places we need to make sure that everything is rounded down, and that we are not creating any tokens.

josojo commented 5 years ago

If I am comparing the different solutions, I like the first posted solution the best. But I am not yet sure about all the consequences. E.g.

bool verifyVolume(Order o, Volume v, Price marketPrices[TOKENS]) {
  // similar process as above
  // v.buyVolume/v.sellVolume == prices[o.fromToken] / prices[o.toToken]
  return v.buyVolume * prices[o.toToken].toAmount * prices[o.fromToken].fromAmount == prices[o.fromToken].toAmount * prices[o.toToken].fromAmount * v.sellVolume
}

here, the volumes and prices need to be picked, so that a valid solution can be found. It would , for example not be possible to have and prices[o.toToken].fromAmount and prices[o.toToken].fromAmount huge primes, which do not share any divisor with prices[o.toToken].toAmount * prices[o.fromToken].fromAmount. It's because in this case, it would not be possible to find ANY volume pair besides 0, to satisfy the equation.

Here is an example: Let's say we work with 4 huge primes:15484901 15484919 15484939 15484951 prices[o.fromToken] / prices[o.toToken] = (15484901/15484951)/(15484939/ 15484919 ) => v.buyVolume 15484939 15484951 == 15484901 15484919 v.sellVolume

Now, we know that v.buyVolume need to be a multiple of 15484901 15484919 . Now, might not be possible to have v.buyvolume = prime1prime2*x && v.buyVolume < order.amount.

twalth3r commented 5 years ago

My take on this would be the following:

An order can be represented by a struct, similar to Felix' proposal. I also added the amount of transacted tokens (execBuyAmount and execSellAmount) and the surplus directly which will make notation easier in the following:

struct Order {
  Account accountId;
  Token sellToken;
  Token buyToken;
  Decimal sellAmount;
  Decimal buyAmount;
  Decimal execSellAmount;
  Decimal execBuyAmount;
  Decimal surplus;
};

All token prices are just Decimals.

Then, we have to check the following:

  1. Uniform Clearing prices

    o.execBuyAmount * prices[o.buyToken] == o.execSellAmount * prices[o.sellToken]
  2. Limit price compliance

    o.execBuyAmount * o.sellAmount >= o.execSellAmount * o.buyAmount
  3. Surplus

    (o.execBuyAmount * o.sellAmount - o.execSellAmount * o.buyAmount) * prices[o.buyToken] == o.surplus * o.sellAmount
  4. Update the balance

    balances[o.accountId][o.sellToken] -= o.execSellAmount;
    balances[o.accountId][o.buyToken] += o.execBuyAmount;

This requires a max of 3 multiplications of Decimals (in the surplus verification). Let me know what you think!

josojo commented 5 years ago

Yeah, @tomtiger87 makes perfect sense for me. Besides your weight factor, its the same definition of surplus, as we had before. Thanks for elaboration. Since it was not obvious for me from the beginning, I am posting it here:

surplus = priceDifference * amount * weight
surplus =  ( o.execBuyAmount/ o.execSellAmount - * ( o.buyAmount / o.sellAmount ) ) *  o.execSellAmount* prices[o.buyToken]
surplus = ( o.execBuyAmount - o.execSellAmount * ( o.buyAmount / o.sellAmount ) ) * prices[o.buyToken]

This also defines surpluses, which do not depend on the choice of order(buy or sell)

surplus = priceDifference * amount * weight
surplus =  ( o.execBuyAmount/ o.execSellAmount - * ( o.buyAmount / o.sellAmount ) ) *  o.execSellAmount* prices[o.buyToken]
surplus =  ( o.execBuyAmount/ o.execSellAmount - * ( o.buyAmount / o.sellAmount ) ) *  o.execBuyAmount* (o.execSellAmount/o.execBuyAmount) *prices[o.buyToken]
surplus =  ( o.execBuyAmount/ o.execSellAmount - * ( o.buyAmount / o.sellAmount ) ) *  o.execBuyAmount* (o.execSellAmount/o.execBuyAmount) *prices[oppositeBuyOrder.buyToken]*(prices[o.buyToken]/prices[oppositeBuyOrder.buyToken])
surplus =  ( (prices[o.buyToken]/prices[oppositeBuyOrder.buyToken])- o.execSellAmount/o.execBuyAmount ) *  o.execBuyAmount*prices[oppositeBuyOrder.buyToken]
surplus =  (( o.buyAmount / o.sellAmount )- o.execSellAmount/o.execBuyAmount ) *  o.execBuyAmount*prices[oppositeBuyOrder.buyToken]
fleupold commented 5 years ago

Thanks @josojo & @tomtiger87 . I'm confused how "3. Surplus" can have a different number of multiplications on the left and right side of the equation.

If we are dealing with relatively large numbers, each multiplication kind of shifts the numbers in a larger range (assuming you have m bits for a decimal a and b, a * b can take up to 2m bits).

Are we missing an implicit multiplication by 1 here or is the surplus denoted in a very large number (2m bits)?

twalth3r commented 5 years ago

@fleupold - I think it's just the definition of surplus as amount * price, so it contains one multiplication.

fleupold commented 5 years ago

@tomtiger87, just to confirm, if we reserve n bits for prices and amounts, we need 2*n bits to encode the surplus?

twalth3r commented 5 years ago

@fleupold - yes, I think so!

twalth3r commented 5 years ago

@fleupold - I just realized that we will need to verify one more constraint in order to make the price vector unique. Previously, this was prices[refToken] == 1. In my model, relating to the notion of an abstract reference token, I'm using

sum(t in tokens) prices[t] / previousPrices[t] == #tokens,

but @josojo rightfully made me aware of the inconveniences of divisions.

So, I will try sum(t in tokens) prices[t] == const and see what that gives.

fleupold commented 5 years ago

Mid term, we should try to represent the amounts/prices that need to go on-chain (e.g. amounts, volume, etc.) with less than 100bits to reduce gas cost for broadcasting them and also lower the amount of bits that need to be hashed inside the snark.

We can probably look at the floating point format that rollUp is going to use; this spreadsheet contains an overview of different mantissas, exponents and suggests that 3 byte (24 bit) should be enough for high precision floating point representations.

Of course, we would have to adjust the optimiser's post processing to convert values accordingly without violating the constraints.