package octez-protocol-017-PtNairob-libs

  1. Overview
  2. Docs
package octez-protocol-017-PtNairob-libs
Legend:
Library
Module
Module type
Parameter
Class
Class type

This module provides the means to test extensively the Liquidity Baking (LB) feature. We recall that this feature is built upon three smart contracts: (1) a CPMM contract initially based on Dexter 2, and (2) two tokens contracts. Our objective is to run “scenarios” consisting in interleaved, realistic calls to these contracts, and to assert these scenarios do not yield any undesirable behaviors.

To that end, three “machines” are provided.

  • The SymbolicMachine allows to simulate scenarios involving the LB feature completely off-chain. It can be seen as an abstraction of the concrete implementation provided by the Tezos node.
  • The ConcreteMachine allows to execute scenarios on-chain.
  • The ValidationMachine combines the two previously mentioned machines. In other words, the ValidationMachine makes the SymbolicMachine and the ConcreteMachine execute the same scenarios, and asserts they remain synchronized after each baked block.

The ValidationMachine allows to (1) validate the SymbolicMachine (i.e., the reimplementation of the LB contracts logic) against the real implementation provided by Tezos, and the contracts originated by the protocol correctly implement the LB logic, as implemented by the SymbolicMachine. That is, the ValidationMachine reports desynchronization of the two machines, but cannot explain this desynchronization.

Machine State Characterization

type xtz = int64
type tzbtc = int
type liquidity = int
type balances = {
  1. xtz : xtz;
  2. tzbtc : tzbtc;
  3. liquidity : liquidity;
}

As far as liquidity baking is concerned, an account can hold three kinds of tokens: xtz, tzbtc, and liquidity.

val pp_balances : Format.formatter -> balances -> unit
type specs = {
  1. cpmm_min_xtz_balance : xtz;
  2. cpmm_min_tzbtc_balance : tzbtc;
  3. accounts_balances : balances list;
}

A value of type specs allows to specify an initial state of a “machine”.

In a nutshell, it consists in specifying the minimal balances of the CPMM contracts and a set of implicit contracts. The two machines provided by this module has a build function which turns a specs into a consistent initial state for this machine.

val pp_specs : Format.formatter -> specs -> unit
type 'a env = private {
  1. cpmm_contract : 'a;
  2. tzbtc_contract : 'a;
  3. tzbtc_admin : 'a;
  4. liquidity_contract : 'a;
  5. liquidity_admin : 'a;
  6. implicit_accounts : 'a list;
  7. holder : 'a;
  8. subsidy : xtz;
}

A value of type 'a env (where 'a is the type of contract identifiers) summarizes the different contracts involved in the LB feature.

Values of type env are constructed by the build function of the machines.

type 'a step =
  1. | SellTzBTC of {
    1. source : 'a;
    2. destination : 'a;
    3. tzbtc_deposit : tzbtc;
    }
  2. | BuyTzBTC of {
    1. source : 'a;
    2. destination : 'a;
    3. xtz_deposit : xtz;
    }
  3. | AddLiquidity of {
    1. source : 'a;
    2. destination : 'a;
    3. xtz_deposit : xtz;
    }
  4. | RemoveLiquidity of {
    1. source : 'a;
    2. destination : 'a;
    3. lqt_burned : liquidity;
    }

A value of type 'a step (where 'a is the type used to identify contracts) describes a consistent sequence of LB smart contract calls.

For instance, SellTzBTC consists in approving an allowance in the TzBTC contract, then calling the token_to_xtz entry point of the CPMM.

val pp_step : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a step -> unit
type 'a state = {
  1. cpmm_total_liquidity : liquidity;
  2. accounts_balances : ('a * balances) list;
}

A summary of the state of a machine, parameterized by the type of contract identifier.

The Symbolic Machine

type contract_id =
  1. | Cpmm
  2. | Holder
  3. | TzBTC
  4. | TzBTCAdmin
  5. | Liquidity
  6. | LiquidityAdmin
  7. | ImplicitAccount of int

In the SymbolicMachine, a contract is identified by a symbolic value.

val pp_contract_id : Format.formatter -> contract_id -> unit
module SymbolicMachine : sig ... end
module ConcreteMachine : sig ... end

A machine that can execute scenarios onchain.

module ValidationMachine : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct