dexter-informal-specification.md 32.8 KB
Newer Older
J H's avatar
J H committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57
# Dexter Exchange: An Informal Specification (Version 1)

This document is an informal specification for Dexter, a contract that can be 
originated on the Tezos blockchain. It is a decentralized token exchange for 
[FA1.2 tokens](https://gitlab.com/tzip/tzip/blob/master/Proposals/TZIP-0007/FA1.2.md). 
Implementation details will mostly be ignored in this document.

# Terminology

For clarity, we will define and highlight certain terms that are used 
throughout the document.

* **XTZ**: the official token on the Tezos blockchain. Also known as 
  tez or colloquially as tezzies. The smallest unit is mutez. The common 
  unit is tez. 1 tez = 1,000,000 mutez. For clarity, we will refer to this 
  token as XTZ.
* **FA1.2**: tokens from a [FA1.2 contract](https://gitlab.com/tzip/tzip/blob/master/Proposals/TZIP-0007/FA1.2.md).
* **token**: tokens from a [FA1.2 contract](https://gitlab.com/tzip/tzip/blob/master/Proposals/TZIP-0007/FA1.2.md) 
  (currently synonymous with FA1.2, but may include other tokens in the future).
* **LQT**: a token that is internal to the dexter exchange contract. It 
  represents the amount of liquidity in a contract relative to the amount 
  **XTZ** and **FA1.2 **held in that contract.
* **exchange contract**: the dexter exchange contract which provides a 
  decentralized exchange on Tezos for **XTZ** and a particular **FA1.2 token**.
* **token contract**: the contract that handles the **FA1.2 token**.
* **xtz_pool**: amount of **XTZ** owned by the liquidity providers of 
  the exchange contract, in mutez. Dexter is responsible for tracking 
  this number because the operation BALANCE is considered unreliable 
  ([Balance Exploit](https://gitlab.com/camlcase-dev/contract-experiments/-/blob/737e6ca0c86970ffae860859028b203e7b685845/receiver-attack/README.md)).
* **token_pool**: amount of **FA1.2** owned by the liquidity providers of the 
  exchange contract. The exchange contract may actually hold more **FA1.2**
  than appears in the **token_pool** stored value for reasons explained below.
* **lqt_total**: total amount of **LQT** in an exchange contract. LQT is owned 
  by contracts/addresses that provide liquidity. It is not owned by the exchange 
  contract itself.
* **sender**: the contract that initiated the current internal transaction, 
  as returned by `SENDER` in Michelson. The sender could be the owner of 
  the liquidity or an intermediate contract that has an **allowance** for a 
  particular owner.
* **allowance**: mechanism whereby one contract (the allower) gives permission 
  to another contract (the allowee) to consume the allower’s **LQT**.
* **manager**: a privileged address that can set the baker of the exchange 
  unless the baker has been frozen.


# The Exchange Contract


## Error Messages

There are no error messages provided by the on chain contract. All `FAILWITH`
will return no message in order to optimize the size of the contract. There is 
a script that automatically removes all error messages from the Michelson 
version and outputs a JSON file with the line number of a fail and the 
corresponding error message.

## Entry Points
58

59
The exchange contract has the following entry points.
60

J H's avatar
J H committed
61 62 63 64 65 66 67 68 69 70
* approve
* addLiquidity
* removeLiquidity
* xtzToToken
* tokenToXtz
* tokenToToken
* updateTokenBalance
* setBaker
* setManager
* default
71 72


J H's avatar
J H committed
73
## Operations
74

J H's avatar
J H committed
75 76 77 78 79
The dexter contract itself is identified in the FA1.2 contract with its own 
address at the entrypoint `default`.  In other words, when transferring FA1.2 
tokens from (resp. to) dexter, the source (resp. target) address given as a 
parameter in the call to the entrypoint transfer from FA1.2 is obtained through 
`SELF; ADDRESS`.
80

J H's avatar
J H committed
81
## Storage
82

J H's avatar
J H committed
83
### Mutable
84

J H's avatar
J H committed
85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102
* **accounts** (big_map of address to pair of amount of LQT it owns and map of 
  address to allowance). For a given address `addr`, we refer to the first 
  component as `accounts[addr].balance` and the second as `accounts[addr].allowance`.
* **lqt_total** (total amount of LQT in a single exchange contract, i.e. the LQT 
  pool)
* **token_pool** (total amount of token that the exchange holds,) the contract 
  implicity calculates the amount it holds without querying the token contract, 
  but there are a few edge cases where it needs to query the token contract to 
  update the amount of token_pool.
* **baker_frozen** if true the manager cannot change the delegate anymore. The 
  idea is that in the future there will be support for a virtual baker and this 
  would be a future proofing solution. Until this is added to the protocol, this 
  should be ignored.
* **self_is_updating_pool_token** boolean flag indicating whether dexter should 
  accept a call on the update token pool internal callback from the token 
  contract. Also, when it is true, only Update Token Pool Internal can be 
  called, all other dexter entry points should fail.
* **xtz_pool** amount of XTZ held by dexter.
103

J H's avatar
J H committed
104
### Immutable
105

J H's avatar
J H committed
106
* **token_address** (address of the FA1.2 token contract)
107

J H's avatar
J H committed
108
#### Invariants (true statements at the end of each contract execution)
109

J H's avatar
J H committed
110 111
* **lqt_total** = sum of the each owner’s LQT balance as given by accounts.
* **xtz_pool** = sum of all XTZ held by Dexter.
112

J H's avatar
J H committed
113
## Fees
J H's avatar
J H committed
114

115
Fees are collected in the two types of trade at the following rates:
J H's avatar
J H committed
116

J H's avatar
J H committed
117 118 119 120
* XTZ to token: 0.3% fee paid in XTZ.
* token to XTZ: 0.3% fee paid in FA1.2 tokens.
* token to token: 0.3% fee paid in input FA1.2 which internally is traded for 
  XTZ, then 0.3% on XTZ which is traded for output token.
J H's avatar
J H committed
121

J H's avatar
J H committed
122 123
Fees collected during trades (XTZ to token, token to XTZ and token to token) add 
value to XTZ and FA1.2 without increasing the number of LQT tokens (**lqt_total**).
124

J H's avatar
J H committed
125
## Implicit parameters
J H's avatar
J H committed
126

127
For all entrypoint calls, we will refer to the following implicit parameters:
J H's avatar
J H committed
128

J H's avatar
J H committed
129 130 131 132
* **sender**: the sender of the entrypoint, as returned by the `SENDER` 
  instruction.
* **amount**: the amount of XTZ, in mutez, in the call, as returned by the 
  `AMOUNT` instruction.
J H's avatar
J H committed
133

J H's avatar
J H committed
134 135 136
Note also that all addresses that are sent as parameters (e.g. to address in 
_Remove Liquidity Entry Point_) should be contracts of type unit. Otherwise the 
contract will fail.
J H's avatar
J H committed
137

J H's avatar
J H committed
138
## Approve Entry Point
J H's avatar
J H committed
139

J H's avatar
J H committed
140 141
The approve entry point sets up an allowance, allowing a contract to burn the 
liquidity of the sender through subsequent calls to remove_liquidity.
J H's avatar
J H committed
142

J H's avatar
J H committed
143
### Parameters
J H's avatar
J H committed
144

J H's avatar
J H committed
145 146 147
* **spender** address: the address of who will be allowed to spend the LQT allowance.
* **allowance** natural: the amount of LQT the spender is allowed to spend for the sender.
* **current_allowance** natural: used to prevent transfer attack as described in [https://docs.google.com/document/d/1YLPtQxZu1UAvO9cZ1O2RPXBbT0mooh4DYKjA_jp-RLM/edit](https://docs.google.com/document/d/1YLPtQxZu1UAvO9cZ1O2RPXBbT0mooh4DYKjA_jp-RLM/edit)
J H's avatar
J H committed
148

J H's avatar
J H committed
149
### Logic
J H's avatar
J H committed
150

J H's avatar
J H committed
151
If **amount** is greater than zero, fail.
152

J H's avatar
J H committed
153 154
If `accounts[sender] `is undefined and **current_allowance** is zero, then an 
account with balance zero and an allowance of **allowance **is defined for spender: 
155 156 157

```
    accounts[sender] := { balance = 0 ; 	
J H's avatar
J H committed
158
    allowance = { spender => allowance } }
159 160
```

J H's avatar
J H committed
161 162 163 164
Otherwise, if `accounts[sender].allowance[spender]` is defined and equal to 
**current_allowance, **or if it is undefined and **current_allowance** equals 0 
then update the map of address to allowance account for the sender to include 
the key spender with the value **allowance**. 
J H's avatar
J H committed
165 166 167 168 169

```
    accounts[sender].allowance[spender] := allowance
```

J H's avatar
J H committed
170
### Operations
171

J H's avatar
J H committed
172
* No operations.
173 174


J H's avatar
J H committed
175
### Errors
176

J H's avatar
J H committed
177 178 179 180 181 182
* **self_is_updating_pool_token** == true
* **amount** is greater than zero
* accounts[sender].allowance[spender] != **current_allowance or 
  **accounts[sender] is defined but not accounts[sender].allowance[spender] and 
  0 != **current_allowance**
* accounts[sender] is undefined and **current_allowance** != **0**
183

J H's avatar
J H committed
184
### Properties
185

J H's avatar
J H committed
186 187 188 189 190 191
* PROP-APR-000: If amount > 0, the operation will fail.
* PROP-APR-001: If accounts[sender].allowance[spender] != **current_allowance**, the operation will fail.
* PROP-APR-002: If accounts[sender] is undefined and **current_allowance** != **0**, the operation will fail.
* PROP-APR-003: If accounts[sender] is undefined and **current_allowance** == 0, then storage will be updated such that accounts[sender].allowance[spender] := allowance.
* PROP-APR-004: If accounts[sender] is defined and accounts[sender].allowance[spender] == **current_allowance**, then storage will be updated such that accounts[sender].allowance[spender] := allowance.
* PROP-APR-005: Assume PROP-APR-003, but spender is sender. The properties should still be true.
192

J H's avatar
J H committed
193
## Add Liquidity Entry Point
194

J H's avatar
J H committed
195
### Parameters
196

J H's avatar
J H committed
197
- **owner** address: the address of the account that will own the LQT.
198

J H's avatar
J H committed
199
- **min_lqt_minted** natural: minimum number of LQT the sender will mint if LQT total is greater than 0.
200

J H's avatar
J H committed
201
- **max_tokens_deposited** natural: maximum number of tokens deposited.
J H's avatar
J H committed
202

J H's avatar
J H committed
203
- **deadline** timestamp: the time after which this transaction can no longer be executed.
J H's avatar
J H committed
204

J H's avatar
J H committed
205
Note: This will trigger an allowance check in the FA1.2 contract for transferring FA1.2 from the **owner** to the exchange if the sender is not the **owner**.
J H's avatar
J H committed
206

J H's avatar
J H committed
207
**tokens_deposited** is the amount of FA1.2 tokens deposited from the owner to the exchange contract. It differs between First Liquidity Provider and Non-First Liquidity Provider.
208

J H's avatar
J H committed
209
### Operations
J H's avatar
J H committed
210 211 212

For both First and Non-First Liquidity Providers.

J H's avatar
J H committed
213
* FA1.2 Transfer **tokens_deposited** from owner to exchange contract
214

J H's avatar
J H committed
215
### Properties
216

J H's avatar
J H committed
217 218 219 220
* PROP-AL-000: if Dexter does not have permission to transfer the owner’s FA1.2 tokens, it will fail.
* PROP-AL-001: if now >= deadline, it will fail.
* PROP-AL-002: if min_lqt_minted == 0, it will fail.
* PROP-AL-003: if max_tokens_deposited == 0, it will fail.
221

J H's avatar
J H committed
222
### Errors
J H's avatar
J H committed
223 224

For both First and Non-First Liquidity Providers.
J H's avatar
J H committed
225 226 227 228 229
* **self_is_updating_pool_token** == true
* now >= **deadline**
* **max_tokens_deposited** == 0 
* **min_lqt_minted** == 0 (no reason to run this if the sender allows zero liquidity to be added) 
* amount == 0
J H's avatar
J H committed
230

J H's avatar
J H committed
231
### First Liquidity Provider
J H's avatar
J H committed
232 233 234

The first liquidity provider sets the initial exchange rate of XTZ to FA1.2.

J H's avatar
J H committed
235
This is called when **lqt_total** is zero.
J H's avatar
J H committed
236

J H's avatar
J H committed
237
If the deadline has passed, i.e. `NOW >= timestamp`, then the transaction fails.
238

J H's avatar
J H committed
239
The initial **lqt_total** is set to be equivalent to the amount of XTZ sent by 
J H's avatar
J H committed
240 241 242 243 244 245
the first liquidity provider, i.e.:

```
    lqt_total := amount 
```

246 247 248

The amount XTC sent by sender is added to the balance of the owner in the exchange. If accounts[owner] does not exist it will be created.

J H's avatar
J H committed
249 250 251 252
```
    accounts[owner].balance := amount
```

J H's avatar
J H committed
253
An internal transaction is generated that calls the token contract, instructing it to transfer **max_tokens_deposited** tokens from the owner to the exchange contract. 
J H's avatar
J H committed
254 255

```
256 257
	token_pool += max_tokens_deposited
	xtz_pool += amount
J H's avatar
J H committed
258 259
```

J H's avatar
J H committed
260
Note: this internal transaction will fail unless the owner has sent a transaction to the token contract beforehand to set up an allowance for the exchange to transfer **max_tokens_deposited** from the owner to exchange.
J H's avatar
J H committed
261

J H's avatar
J H committed
262
Note: If the owner does not have at least **max_tokens_deposited** at the token contract, then the token contract will fail, hence cancelling the whole operation. 
263 264


J H's avatar
J H committed
265
#### Properties 
266

J H's avatar
J H committed
267 268
* PROP-AL-004: if now is less than deadline, lqt_pool is zero, min_lqt_minted is greater than zero and less than or equal to amount, amount is greater than or equal to one tez, Dexter has permission to transfer max_tokens_deposited from owner’s FA1.2 tokens, owner has at least max_tokens_deposited FA1.2 tokens and token_address is a FA1.2 contract, then it should succeed.
* PROP-AL-005: Assume PROP-AL-004, then storage will be updated such that lqt_total := amount, token_pool += max_tokens_deposited, xtz_pool += amount.
269

J H's avatar
J H committed
270
#### Errors
271

272
For only the first liquidity provider.
J H's avatar
J H committed
273

J H's avatar
J H committed
274
* amount < 1tz
J H's avatar
J H committed
275 276


J H's avatar
J H committed
277
### Non-First Liquidity Provider
278 279

Note: Adding liquidity requires the sender contract to provide an equivalent exchange value of XTZ and FA1.2, meaning x of XTZ can be traded for y of FA1.2.
J H's avatar
J H committed
280

J H's avatar
J H committed
281
This is called when **lqt_total** is greater than zero.
J H's avatar
J H committed
282

J H's avatar
J H committed
283
If the deadline has passed, i.e. NOW >= timestamp, then the transaction fails.
J H's avatar
J H committed
284

J H's avatar
J H committed
285
The sender provides a minimum amount of LQT they want to create (**min_lqt_minted**), the amount of XTZ they want to provide (**amount**) and the maximum number of FA1.2 they want to provide (**max_tokens_deposited)**.
J H's avatar
J H committed
286 287 288

The amount of LQT created is:

289

J H's avatar
J H committed
290
```
291
    lqt_created = floor(lqt_total * amount / xtz_pool)
J H's avatar
J H committed
292 293
```

294

J H's avatar
J H committed
295
If `lqt_created` is lower than the amount of LQT they want to create, **min_lqt_minted**, the transaction will fail. If `xtz_pool` is zero, the transaction will fail.
J H's avatar
J H committed
296

J H's avatar
J H committed
297
Otherwise, **lqt_total** is updated to contain the newly created liquidity:
J H's avatar
J H committed
298

299

J H's avatar
J H committed
300 301 302 303
```
    lqt_total := lqt_total + lqt_created
```

304

J H's avatar
J H committed
305 306
The newly created liquidity is added to the balance of the owner in exchange:

307

J H's avatar
J H committed
308 309 310 311
```
    accounts[owner].balance += lqt_created
```

312

J H's avatar
J H committed
313 314
The amount of FA1.2 to be deposited is:

315

J H's avatar
J H committed
316
```
J H's avatar
J H committed
317
    tokens_deposited = ceil(token_pool * amount / xtz_pool).
J H's avatar
J H committed
318
```
J H's avatar
J H committed
319

J H's avatar
J H committed
320

J H's avatar
J H committed
321
If `tokens_deposited` is greater than the maximum number they want to provide, `max_tokens_deposited`, the transaction will fail. If `tokens_deposited` is zero, the transaction will fail.  If `xtz_pool` is zero, the transaction will fail.
322 323 324

An internal transaction is emitted that calls the token contract, instructing it to transfer `tokens_deposited` tokens from the owner to the exchange contract. 

J H's avatar
J H committed
325

J H's avatar
J H committed
326
```
327
	token_pool += tokens_deposit
J H's avatar
J H committed
328
    xtz_pool += amount
J H's avatar
J H committed
329
```
J H's avatar
J H committed
330

J H's avatar
J H committed
331
#### Properties
332

J H's avatar
J H committed
333 334
* PROP-AL-006:  if now is less than deadline, lqt_pool is greater than zero, min_lqt_minted is greater than zero, tokens_deposited less than or equal to max_tokens_deposited, amount is greater than zero, Dexter has permission to transfer tokens_deposited from owner’s FA1.2 tokens, owner has at least tokens_deposited FA1.2 tokens and token_address is a FA1.2 contract, then it should succeed.
* PROP-AL-007: Assume PROP-AL-006, then storage will be updated such that lqt_total := floor(lqt_total * amount / xtz_pool), accounts[owner].balance := floor(lqt_total * amount / xtz_pool), token_pool += tokens_deposit and xtz_pool += amount.
335 336


J H's avatar
J H committed
337
#### Errors
J H's avatar
J H committed
338

J H's avatar
J H committed
339
For only non-first liquidity provider.
J H's avatar
J H committed
340

J H's avatar
J H committed
341 342 343 344
* tokens_deposited == 0
* **max_tokens_deposited** < tokens_deposited
* lqt_created < **min_lqt_minted**
* **xtz_pool** == 0
345

J H's avatar
J H committed
346
## Remove Liquidity Entry Point
347 348 349

LQT tokens can be burned (or destroyed) in order to withdraw a proportional amount of XTZ and FA1.2. They are withdrawn at the current exchange rate.

J H's avatar
J H committed
350
### Parameters
351

J H's avatar
J H committed
352 353 354 355 356 357
* **owner**: address which owns the LQT that will be burned.
* **to**: address where to send the XTZ and FA1.2 tokens.
* **lqt_burned** natural: amount of LQT the sender wants to burn
* **min_xtz_withdrawn** mutez: the minimum amount of XTZ (in Mutez) the sender wants to withdraw and send.
* **min_tokens_withdrawn** natural: the minimum amount of FA1.2 Tokens the sender wants to withdraw and send.
* **deadline** timestamp: the time after which this transaction can no longer be executed
358

359

J H's avatar
J H committed
360
### Allowance Check
J H's avatar
J H committed
361

362
Burning LQT requires an allowance check if the sender is not the owner. If the sender does not have permission then it will fail. If the sender has permission, but the amount exceeds their allowance then it will fail.
J H's avatar
J H committed
363

364
Allowance is added through the approve entry point. When a contract A is given an allowance of X LQT for contract B, it is allowed to burn up to X LQT for A. 
J H's avatar
J H committed
365

366
Note: A liquidity owner will also need to give a Dexter contract permission to spend its FA1.2 tokens. The rules are defined in the [FA1.2 contract](https://gitlab.com/tzip/tzip/blob/master/A/FA1.2.md). This should be handled by a dApp.
J H's avatar
J H committed
367

J H's avatar
J H committed
368

J H's avatar
J H committed
369
### Logic
J H's avatar
J H committed
370

J H's avatar
J H committed
371
If **amount** is greater than zero, fail.
J H's avatar
J H committed
372

J H's avatar
J H committed
373
If the deadline has passed, i.e. NOW >= timestamp, then the transaction fails.
J H's avatar
J H committed
374

J H's avatar
J H committed
375
Require LQT balance check. Verify that `accounts[owner]` is defined and that
376

J H's avatar
J H committed
377 378 379
```
    accounts[owner].lqt >= lqt_burned
```
380 381 382

Otherwise fail.

J H's avatar
J H committed
383 384
Requires allowance check for lqt_burned. That is, unless sender = owner, verify that

385

J H's avatar
J H committed
386
```
387
    accounts[owner].allowance[sender] >= lqt_burned
J H's avatar
J H committed
388 389
```

390

J H's avatar
J H committed
391 392
And otherwise fail (as described below). If successful, remove the burnt LQT from allowance:

393

J H's avatar
J H committed
394
```
395
    accounts[owner].allowance[sender] -= lqt_burned
J H's avatar
J H committed
396 397
```

398

J H's avatar
J H committed
399 400 401 402
The sender provides the amount of LQT they want to burn in the lqt_burned 
parameter, and the minimum amount of XTZ and FA1.2 they want to withdraw, in the
min_xtz_withdrawn and min_tokens_withdrawn parameters respectively. If either 
limits are not met then the transaction will fail.
J H's avatar
J H committed
403 404 405 406 407

The amount of XTZ withdrawn is 

```
    xtz_withdrawn = floor(xtz_pool * lqt_burned / lqt_total). 
408
    xtz_pool -= xtz_withdrawn
J H's avatar
J H committed
409 410
```

411

J H's avatar
J H committed
412 413 414
If `lqt_total` is zero, the transaction will fail. If `xtz_pool < xtz_withdrawn`, the transaction will fail.

This is implemented by the emission of an internal transaction that transfers xtz_withdrawn to the **to** address.
J H's avatar
J H committed
415 416 417

The amount of FA1.2 withdrawn is:

418

J H's avatar
J H committed
419
```
J H's avatar
J H committed
420 421
    tokens_withdrawn = floor(token_pool * lqt_burned / lqt_total).
    token_pool -= tokens_withdrawn 
J H's avatar
J H committed
422 423
```

424

J H's avatar
J H committed
425 426 427
The latter subtraction will fail if **tokens_withdrawn** > **token_pool**.

This is implemented by the emission of an internal operation that calls the token contract, instructing it to transfer the tokens_withdrawn amount of tokens from the exchange contract to the **to** address.
J H's avatar
J H committed
428 429 430

Finally, the balance of the owner and the total supply is updated :

431

J H's avatar
J H committed
432 433 434 435 436
```
    accounts[owner].balance -= lqt_burned
    lqt_total -= lqt_burned 
```

J H's avatar
J H committed
437
The latter subtraction will fail if **lqt_burned** > **lqt_total**.
438

J H's avatar
J H committed
439
### Operations
440

J H's avatar
J H committed
441 442
*   Send **xtz_withdrawn** from exchange to **to** address.
*   FA1.2 Transfer **tokens_deposited** from exchange contract to **to** address.
443

J H's avatar
J H committed
444
### Errors
445

J H's avatar
J H committed
446 447 448 449 450 451 452 453 454 455 456 457 458 459 460
* **self_is_updating_pool_token** == true
* now >= deadline
* amount > 0
* min_xtz_withdrawn == 0
* min_tokens_withdrawn == 0 
* lqt_burned == 0
* lqt_burned > accounts[owner].balance or if accounts[owner] is undefined
* lqt_burned > accounts[owner].allowances[sender] when sender != owner or if accounts[owner].allowances[sender] is undefined
* xtz_withdrawn < min_xtz_withdrawn
* **lqt_total** == 0 (implicit from the division)
* tokens_withdrawn < min_tokens_withdrawn
* tokens_withdrawn < token_pool
* xtz_withdrawn < xtz_pool (implicitly by the subtraction)
* lqt_burned > lqt_total
* To address does not have the parameter type unit.
461

J H's avatar
J H committed
462
### Properties
463

J H's avatar
J H committed
464 465 466 467 468 469 470 471 472 473 474
* PROP-RL-000: If amount > 0, the operation will fail.
* PROP-RL-001: If **deadline** >= NOW, the operation will fail.
* PROP-RL-002: If min_xtz_withdrawn == 0, the operation will fail.
* PROP-RL-003: If min_token_withdrawn == 0, the operation will fail.
* PROP-RL-004: If xtz_withdrawn < min_xtz_withdrawn, the operation will fail.
* PROP-RL-005: If token_withdraw < min_token_withdrawn is zero, the operation will fail.
* PROP-RL-006: If lqt_burned > accounts[owner].balance, the operation will fail.
* PROP-RL-007: If sender != owner and lqt_burned > account[owner].allowances[sender], the operation will fail.
* PROP-RL-008: If **to **or its provided entry point do not have parameter of type unit, this operation will fail.
* PROP-RL-009: For any **deadline** value less than NOW, **min_xtz_withdrawn** greater than zero, **min_tokens_withdrawn** greater than zero, **xtz_withdrawn** greater than or equal to **min_xtz_withdrawn**, **tokens_withdrawn** greater than or equal to **min_tokens_withdrawn**, **lqt_burned **less than or equal to **accounts[owner].balance**, if **to **has a parameter of unit (or is an entrypoint with parameter unit), **tokens_withdrawn **will be given to **to **via the **token_address** contract and **xtz_withdrawn **will be sent to **to**. 
* PROP-RL-010: Assume PROP-RL-009, then storage will be updated such that **lqt_total** -= **lqt_burned**, **xtz_pool** -= **xtz_withdrawn**, **token_pool** -= **tokens_withdrawn**, and** accounts[owner].balance** -= **lqt_burned**.
475

J H's avatar
J H committed
476
## XTZ to Token Entry Point
J H's avatar
J H committed
477

J H's avatar
J H committed
478
### Parameters
J H's avatar
J H committed
479

J H's avatar
J H committed
480 481 482
* **to** address: address to send the FA1.2 tokens to. 
* **min_tokens_bought** natural: minimum amount of tokens the sender wants to buy.
* **deadline** timestamp: the time after which this transaction can no longer be executed.
J H's avatar
J H committed
483

J H's avatar
J H committed
484
### Logic
485

J H's avatar
J H committed
486
If the deadline has passed, i.e. NOW >= timestamp, then the transaction fails.
J H's avatar
J H committed
487

J H's avatar
J H committed
488
If amount == 0, then the transaction will fail.
489

J H's avatar
J H committed
490
If min_tokens_bought == 0, then the transaction fails. 
J H's avatar
J H committed
491

J H's avatar
J H committed
492
If xtz_pool == 0 or token_pool == 0, then the transaction fails. 
493

J H's avatar
J H committed
494 495
A fee of %0.3 is taken. This is implemented thus:

496

J H's avatar
J H committed
497 498 499
```
    tokens_bought = floor((amount * 997 * token_pool) / 
            (xtz_pool * 1000 + (amount * 997)))
500 501
    token_pool -= tokens_bought
    xtz_pool += amount
J H's avatar
J H committed
502 503
```

J H's avatar
J H committed
504
**tokens_bought** must be greater than or equal to **min_tokens_bought** or it will fail.
505

J H's avatar
J H committed
506
**token_pool** must be larger or equal to **tokens_bought**, or the transaction will fail.
J H's avatar
J H committed
507

508 509 510 511
The `to `address receives the FA1.2 equivalent to `tokens_bought`. This is implemented by the emission of an internal operation that calls the token address, instructing it to transfer `tokens_bought` tokens from the exchange contract to `to address`.

lqt_total and balance are unaffected. 

J H's avatar
J H committed
512
### Operations
513

J H's avatar
J H committed
514
* FA1.2 Transfer tokens_bought from exchange contract to **to** address.
515

J H's avatar
J H committed
516
### Errors
J H's avatar
J H committed
517

J H's avatar
J H committed
518 519 520 521 522 523 524 525
* **self_is_updating_pool_token** == true
* now >= deadline
* amount == 0
* min_tokens_bought == 0
* **xtz_pool** == 0
* **token_pool** == 0
* min_tokens_bought > tokens_bought
* tokens_bought > token_pool
J H's avatar
J H committed
526

J H's avatar
J H committed
527
### Properties
528

J H's avatar
J H committed
529 530 531 532 533
* PROP-XTT-000: If **now** >= **deadline**, this operation will fail.
* PROP-XTT-001: If **min_tokens_bought** == 0, this operation will fail. 
* PROP-XTT-002: If **tokens_bought** < **min_tokens_bought**, this operation will fail.
* PROP-XTT-003: If **xtz_pool **or **token_pool** is zero, this operation will fail.
* PROP-XTT-004: If **now** < **deadline**, **min_tokens_bought** > 0, **min_tokens_bought** <= **tokens_bought**, and **tokens_bought** <= **token_pool**, then storage will be updated such that **xtz_pool** += **amount**, **token_pool** -= **tokens_bought** and **tokens_bought** will be transferred to the **to** address.
J H's avatar
J H committed
534

J H's avatar
J H committed
535
## Token to XTZ Entry Point
J H's avatar
J H committed
536

J H's avatar
J H committed
537
### Parameters
538

J H's avatar
J H committed
539 540 541 542 543
* **owner** address: the address that owns that FA1.2 that are being sold
* **to** address: address to send the XTZ tokens to. 
* **tokens_sold** natural: the number of tokens the sender wants to sell.
* **min_xtz_bought** mutez: minimum amount of XTZ (in Mutez) the sender wants to purchase.
* **deadline** timestamp: the time after which this transaction can no longer be executed.
J H's avatar
J H committed
544

J H's avatar
J H committed
545
### Logic
546

J H's avatar
J H committed
547
If the deadline has passed, i.e. `NOW >= timestamp`, then the transaction fails.
548

J H's avatar
J H committed
549
If **amount** is greater than zero, fail.
550

J H's avatar
J H committed
551
If xtz_pool == 0 or token_pool == 0, then the transaction fails. 
552

J H's avatar
J H committed
553
If **min_xtz_bought** == 0, fail.
J H's avatar
J H committed
554

555
Note: Requires allowance check in the FA1.2 contract for transferring FA1.2 from the owner to the exchange.
J H's avatar
J H committed
556 557 558 559

A fee of %0.3 is taken. This is implemented thus:

```
560
    xtz_bought = floor((tokens_sold * 997 * xtz_pool) / 
J H's avatar
J H committed
561
            (token_pool * 1000 + (tokens_sold * 997)))
562 563
    token_pool += tokens_sold
    xtz_pool -= xtz_bought
J H's avatar
J H committed
564 565
```

J H's avatar
J H committed
566
If **min_xtz_bought** > **xtz_bought**, then the contract fails. 
J H's avatar
J H committed
567

J H's avatar
J H committed
568
The **to** address receives XTZ equivalent to `xtz_bought`. This is implemented by the emission
569 570 571 572

of an internal operation that transfers this sum to the `to address`.

The exchange contract receives FA1.2 equivalent to `tokens_sold`. This is implemented by the emission of an internal operation that calls token, instructing it to transfer `tokens_sold` tokens from the `owner` to the exchange contract.
J H's avatar
J H committed
573 574 575 576

`lqt_total` and `balance` are unaffected (Note: assuming that amount is zero). 


J H's avatar
J H committed
577
### Operations
578

J H's avatar
J H committed
579 580
* Transfer XTZ from exchange to **to** address. (with type unit)
* FA1.2 Transfer **tokens_sold** from  **to** address to exchange contract.
581

J H's avatar
J H committed
582
### Errors
J H's avatar
J H committed
583

J H's avatar
J H committed
584 585 586 587 588 589 590 591
* **self_is_updating_pool_token** == true
* now >= **deadline**
* **min_xtz_bought** > xtz_bought
* **amount** > 0
* **token_pool** == 0
* **xtz_pool** == 0
* **min_xtz_bought** == 0
* **tokens_sold** == 0
J H's avatar
J H committed
592

J H's avatar
J H committed
593
### Properties
594

J H's avatar
J H committed
595 596 597 598 599 600
* PROP-TTX-000: If **now** >= **deadline**, this operation will fail.
* PROP-TTX-001: If **min_xtz_bought** == 0, this operation will fail. 
* PROP-TTX-002: If **xtz_bought** < **min_xtz_bought**, this operation will fail.
* PROP-TTX-003: If **amount **!= zero, this operation will fail.
* PROP-TTX-004: If **xtz_pool **or **token_pool** is zero, this operation will fail.
* PROP-TTX-005: If **now** < **deadline**, **min_xtz_bought** > 0, **min_xtz_bought** <= **xtz_bought**, and **xtz_bought** <= **xtz_pool**, then storage will be updated such that **xtz_pool** -= **xtz_boughtZ**, **token_pool** += **tokens_sold** and **xtz_bought** will be transferred to the **to** address.
601

J H's avatar
J H committed
602
## Token to Token Entry Point
603

604
Token to token allows two Dexter contracts to interoperate and perform a trade between them so an owner of one FA1.2 to token and trade for another FA1.2 token in a single transaction.
605

J H's avatar
J H committed
606
### Parameters
607

J H's avatar
J H committed
608 609 610 611 612 613
* **output_dexter_address**: address of Dexter exchange of FA1.2 that the sender wants to purchase
* **min_tokens_bought**: minimum amount of tokens the sender will purchase from **output_dexter_address**
* **owner** address: the address that owns that FA1.2 that are being sold
* **to** address: address to send the XTZ tokens to. 
* **tokens_sold** natural: the number of tokens the sender wants to sell.
* **deadline** timestamp: the time after which this transaction can no longer be executed.
614

J H's avatar
J H committed
615
### Logic
616

J H's avatar
J H committed
617
If the deadline has passed, i.e. `NOW >= timestamp`, then the transaction fails.
618

J H's avatar
J H committed
619
If **amount** is greater than zero, fail.
620

J H's avatar
J H committed
621
If `min_tokens_bought` is zero, the transaction will fail.
622

J H's avatar
J H committed
623
If `tokens_pool` is zero, the transaction will fail. If `xtz_pool` is zero, the transaction will fail.
624

J H's avatar
J H committed
625
Note: Requires allowance check in the FA1.2 contract for transferring FA1.2 from the owner to the exchange, and for the **output_dexter_address **to the **to **address.
626

J H's avatar
J H committed
627
This entrypoint performs the same exchange as token to XTZ, then with the XTZ from that exchange, it performs an XTZ to Token transaction with that XTZ by sending it to **output_dexter_address.**
628

629 630 631 632

```
    xtz_bought = floor((tokens_sold * 997 * xtz_pool) / 
            (token_pool * 1000 + (tokens_sold * 997)))
633 634
    token_pool += tokens_sold
    xtz_pool -= xtz_bought
635 636 637
```


J H's avatar
J H committed
638
Call “XTZ to token” of the **output_dexter_address **with the following parameters: **to, min_tokens_bought** and **deadline**, and include XTZ amount **xtz_bought**. This will trigger a transfer of tokens from **output_dexter_address** to **to.**
639

J H's avatar
J H committed
640
Send **tokens_sold** from **owner **to the dexter contract which was called by the **sender**.
641 642


J H's avatar
J H committed
643
### Operations
644

J H's avatar
J H committed
645 646
* token_address%transfer
* **output_dexter_address**%xtzToToken (this will cause **output_dexter_address** to call **output_dexter_address**.storage.token_address%transfer to **to **address)
647

J H's avatar
J H committed
648
### Errors
649

J H's avatar
J H committed
650 651 652 653 654 655 656
* **self_is_updating_pool_token** == true
* now >= **deadline**
* amount > 0
* **min_tokens_bought** == 0
* **xtz_pool** == 0
* **token_pool** == 0
* **tokens_sold** == 0
657

J H's avatar
J H committed
658
### Properties
659

J H's avatar
J H committed
660 661 662 663 664
* PROP-TTT-000: If **now** >= **deadline**, then this operation will fail.
* PROP-TTT-001: If **output_dexter_address **is not a Dexter contract, this operation will fail.
* PROP-TTT-002: If **min_tokens_bought** == 0, this operation will fail.
* PROP-TTT-003: If **tokens_bought **< **min_tokens_bought**, this operation will fail.
* PROP-TTT-004: If **tokens_bought **>= **min_tokens_bought**, dexter has permission for owner’s **tokens_sold **and **tokens_sold** <= owner’s balance, **now** < **deadline**, then this operation will succeed.
665

J H's avatar
J H committed
666
## Update Token Balance Entry Point
667

J H's avatar
J H committed
668 669 670 671 672
There are a few edge cases where **token_pool **can become out of sync with the 
value that the dexter exchange actually holds in **token**. For example, someone 
sends the exchange contract token for free or the **token** has some behavior 
where the owner’s token automatically increases or decreases. This entrypoint 
updates the token balance of dexter.
673

J H's avatar
J H committed
674
### Parameters
675

J H's avatar
J H committed
676
* sender_key_hash: key_hash
677

J H's avatar
J H committed
678
### Logic
679

J H's avatar
J H committed
680
Only an implicit account is allowed to call Update Token Pool in order to prevent smart contracts calling it and inserting operations in unexpected ways (which could possibly cause fa1.2%getBalance to return an unexpected value). 
681

J H's avatar
J H committed
682
This is enforced by converting **sender_key_hash** (only implicit accounts have key hashes) to an address and making sure it is equal to the sender.
J H's avatar
J H committed
683 684

```
J H's avatar
J H committed
685
	assert(sender == address(implicit_account(sender_key_hash)))
J H's avatar
J H committed
686 687
```

J H's avatar
J H committed
688
To prepare for Update Token Balance Internal, set the storage value of **self_is_updating_pool_token** to true.
689

J H's avatar
J H committed
690
**self_is_updating_pool_token` := true`**
691

J H's avatar
J H committed
692
Then call the %getBalance entrypoint of the token contract and pass in the address of the Dexter contract at Update Token Balance Internal entrypoint.
693 694 695 696 697

```
	transfer(((), self%updateTokenBalanceInternal), 0, token_address%getBalance)
```

J H's avatar
J H committed
698
### Operations
699

J H's avatar
J H committed
700
* Call FA1.2 %getBalance for dexter's address with callback set to the entrypoint Update Token Balance Internal of the dexter contract itself.
701

J H's avatar
J H committed
702
### Errors
703

J H's avatar
J H committed
704 705 706
* **sender_key_hash** != sender
* amount is greater than zero
* **self_is_updating_pool_token **is true
707

J H's avatar
J H committed
708
### Properties
709

J H's avatar
J H committed
710 711 712
* PROP-UTB-000: If xtz sent is greater than zero, this operation will fail. (All other PROP-UTB properties assume that AMOUNT is zero).
* PROP-UTB-001: If the contract at **token_address **does not have a getBalance entrypoint, it will fail (the originator of the contract is responsible for making sure **token_address **points to a valid FA1.2 contract).
* PROP-UTB-002: If the contract at **token_address **has a getBalance entrypoint with the expected type signature, and the expected properties of Update Token Balance Internal are met, then **token_pool** will be updated and **self_is_updating_pool_token** will be false.
713

J H's avatar
J H committed
714
## Update Token Balance Internal Entry Point
715

J H's avatar
J H committed
716
This is the callback from the token contract. Only the token contract can call this entry point. And the call is only accepted when **self_is_updating_pool_token** is true**.** 
717

J H's avatar
J H committed
718
### Parameters
719

J H's avatar
J H committed
720
* token_pool nat
721

J H's avatar
J H committed
722
### Logic
723

J H's avatar
J H committed
724
First, assert that the **sender** is **token** and that **self_is_updating_pool_token** is true Then, update the token balance as per the parameter, and reset the **self_is_updating_pool_token** flag**.**
725 726 727


```
J H's avatar
J H committed
728 729
    token_pool := token_pool
    self_is_updating_token_pool := false
730 731
```

J H's avatar
J H committed
732
### Operations
J H's avatar
J H committed
733

734
None
J H's avatar
J H committed
735

J H's avatar
J H committed
736
### Errors
J H's avatar
J H committed
737

J H's avatar
J H committed
738 739 740
* amount is greater than zero
* sender != token
* self_is_updating_token_pool != true
741

J H's avatar
J H committed
742
### Properties
743

J H's avatar
J H committed
744 745 746 747
* PROP-UTBI-000: Regardless of other parameter values, if xtz sent is greater than zero, this operation will fail. (All other PROP-UTBI properties assume that AMOUNT is zero).
* PROP-UTBI-001: For any **sender** that is not equal to **token_address**, the operation will fail.
* PROP-UTBI-002: For any **sender** that is equal to **token_address**, and **self_is_updating_pool_token** is not true, the operation will fail.
* PROP-UTBI-003: For any **sender** that is equal to **token_address**, and **self_is_updating_pool_token** is true, storage **token_pool **will be set to parameter **token_pool**, and **self_is_updating_pool_token **will be set to false.
748

J H's avatar
J H committed
749
## Set Baker
750

J H's avatar
J H committed
751 752 753 754 755 756
The manager has the right to set the baker for a Dexter contract. This is a 
compromise because proposed baker voting or bidding systems are currently not 
practical in Tezos. The rewards are paid to the Dexter contract and divided 
amongst the liquidity providers by the percentage of LQT tokens that they own. 
The idea behind freezing the baker is to give up the manager rights and set a 
virtual baker when it is supported in the protocol https://forum.tezosagora.org/t/on-the-tezos-delegation-model/1562/4.
757

J H's avatar
J H committed
758
### Parameters
759

J H's avatar
J H committed
760 761
* new_baker: option(key_hash)
* freeze_baker: bool
762

J H's avatar
J H committed
763
### Logic
764

J H's avatar
J H committed
765
If **amount** is greater than zero, fail.
766

767
If sender == storage.manager and not storage.baker_frozen then 
768 769

```
J H's avatar
J H committed
770 771
    set_delegate(new_baker)
    if (freeze_baker) then baker_frozen := true
772 773
```

774
Otherwise fail
775

J H's avatar
J H committed
776
### Operations
777

J H's avatar
J H committed
778
* SET_DELEGATE
779

J H's avatar
J H committed
780
### Errors
781

J H's avatar
J H committed
782 783 784 785 786
* **self_is_updating_pool_token** == true
* Amount is greater than zero
* Sender is not the manager
* The baker is frozen
* Amount is greater than zero
787

J H's avatar
J H committed
788
### Properties
789

J H's avatar
J H committed
790 791 792 793
* PROP-SB-000: If amount > zero, this operation will fail.
* PROP-SB-001: If sender is not manager, this operation will fail.
* PROP-SB-002: If freezeBaker is true, this operation will fail.
* PROP-SB-003: If sender is the manager and storage.baker_frozen is false, then a set_delegate(new_baker) operation will be emitted and storage.baker_frozen := **freeze_baker**.
794

J H's avatar
J H committed
795
## Set Manager
796 797 798

The manager can set a new address as the manager of the Dexter contract.

J H's avatar
J H committed
799
### Parameters
800

J H's avatar
J H committed
801
* new_manager: address
802

J H's avatar
J H committed
803
### Logic
804