### DEX predicates + OVM

On this call, I would like to discuss OVM and predicates, that we need for DEX futures implementation. I’ve got some writing notes, that I will share with you along with Ivan, who actively participated in this research.

**We will provide additional comments on the call.** *In the future I will make a post about that.*

#### Simplest Case:

- Suppose that there is only 1 futures contract
- Suppose that every trader can only have 1 “relationship” with a contract (if the trader has sold the contract, then he can not buy this contract in this cycle anymore)

So we need to define 3 predicates:

`isTransfer (A , B)`

`existContract (A , B)`

`isSet(A , B , Condition)`

#### Scenario 1

We assume that there are only 2 traders: Alice and Bob

Let `isSet ( . , . )`

- function from two arguments that takes true or false value.

#### Example:

`isSet (A, B) = 1`

-> there is settlement between A and B

`isSet (A, B) = 0`

-> there is NO settlement between A and B

The **execution of a futures contract** can be written down as follows:

There is a day, when - `isSet (A, B) = 1`

Let `isTransfer (. , .)`

- function from 2 arguments, that takes `true`

or `false`

.

Example: `isTransfer (. , .) =1`

-> (A sells her contract to B) or (b sells his contract to A)

#### Scenario 2

There are 3 traders: Alice, Bob and Chris. Suppose that Alice has a contract with Bob

Consider the core of the future A has a contract with B

With OVM we can limit variants of possible future:

This could be a great way of creating DEX. If there are supplemented, of the logic of DEX can be described in the predicate language.