Skip to main content

Assertions

Assertions

Denaria, in collaboration with the Phylax team, has implemented an innovative security system. Thanks to the Credible Layer technology, it is possible to define rules, called assertions, which, if not satisfied, cause transactions to be excluded and therefore not executed.

This technology allows the introduction of rules that must hold for transactions interacting with specific contracts. When a transaction interacts with a contract that is subject to an assertion, the rule is evaluated; if it is not satisfied, the sequencer does not include the transaction in the block, and it is therefore not executed.

Bad Debt Assertions​

The first assertion we implemented follows this logic: Any user cannot cause bad debt to himself as a result of his transaction. This rule translates into the following mathematical formulation: For any user U and any transaction T that interacts with user U:

Let:
PnL_post(U) = PnL(U) after transaction T
Collateral_post(U) = Collateral(U) after transaction T
Then the following invariant must hold:
Collateral_post(U) + PnL_post(U) ≥ 0

Any transaction that does not satisfy this rule is not included in the block at the sequencer level and therefore not validated by the chain.

This assertion prevents some:

  • Protocol bugs that cause unexpected losses.
  • Economic attacks that intentionally produce bad debt.
  • Implementation errors in protocol operations.

And still allows:

  • Normal protocol operations (trades, liquidity deposits, and withdrawals).
  • Legitimate liquidations, which may cause bad debt without failing the assertion.