This module provides a set of abstractions to reason about the so-called “liquidity baking” feature1.
1: https://gitlab.com/tezos/tzip/-/blob/master/drafts/current/draft-liquidity_baking.md
We remind that this feature is built upon three smart contracts: (1) a CPMM contract initially based on Dexter 2, and (2) two tokens contracts.
Our purpose for Liquidity Baking is to easily express and test invariants regarding the execution of these contracts. To that end, we have introduced a set of dedicated types to describe arbitrary contexts in terms of account balances (see Liquidity_baking_machine.specs), along with build functions that turn a description of a context into concrete states.
In this module, we provide QCheck generators which allow to construct arbitrary specifications for states, and so-called scenarios (i.e., sequences of entrypoint calls).
val arb_specs :
Liquidity_baking_machine.tzbtc ->
Liquidity_baking_machine.liquidity ->
Liquidity_baking_machine.specs QCheck.arbitraryarb_specs max_tzbtc max_liquidity constructs arbitrary Liquidity Baking specs for an initial state, where at most max_tzbtc and max_liquidity are shared among an arbitrary number of implicit accounts.
val arb_scenario :
Liquidity_baking_machine.tzbtc ->
Liquidity_baking_machine.liquidity ->
int ->
(Liquidity_baking_machine.specs
* Liquidity_baking_machine.contract_id Liquidity_baking_machine.step list)
QCheck.arbitraryarb_scenario max_tzbtc max_liquidity size constructs arbitrary Liquidity Baking specs with a semantics similar to arb_specs, along with sequences of valid scenarios (i.e., sequences of entrypoint calls) of length size. By valid, we mean that running the scenario using a Liquidity baking machine initialized with the specs should succeed.
val arb_adversary_scenario :
Liquidity_baking_machine.tzbtc ->
Liquidity_baking_machine.liquidity ->
int ->
(Liquidity_baking_machine.specs
* Liquidity_baking_machine.contract_id
* Liquidity_baking_machine.contract_id Liquidity_baking_machine.step list)
QCheck.arbitraryarb_adversary_scenario max_tzbtc max_liquidity size constructs arbitrary scenarios that can be used to challenge the “no global gain” property of Liquidity Baking.
The key idea of this property is the following: a given contract cannot profit from Liquidity Baking if they are the only one to interact with the CPMM (in the absence of subsidies). The scenario generated by arb_adversary_scenario only consists in step performed by one contract. This contract is identified by the contract_id returned by this function.