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 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.
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.