runtimeverification / plutus-core-semantics

BSD 3-Clause "New" or "Revised" License
27 stars 5 forks source link

Notes on Djed #303

Open ChristianoBraga opened 2 years ago

ChristianoBraga commented 2 years ago

Notes on Djed

Introduction

- Djed is an algorithmic stablecoin protocol. - A stablecoin is a cryptocurrency that is backed by ressources in a [fiat](https://en.wikipedia.org/wiki/Fiat_money) currency. * The main motivation for stablecoins is the instability of cryptocurrencies. - It has mechanisms to maintain a low deviation of its price from a target price. * The most common mechanism is to back the stablecoin by reserves and use these reserves to buy and sell stablecoins to keep its price close to a target price. - Revenue for the operator comes from the investments made with the reserves. * The liquidity of the reserves guarantees the ability of the operator to react to changes in the price and may compromise its stability. * Fees (spread) when buying and selling coins are also a source of revenue. - Requires trust on the entities keeping the reserves. * This is where cryptocurrencies enter the scene. Blockchains are reliable and smartcontracts form a transparent way to implement stabilization measures. - DJed act as an autonomous bank: * It has a reserve R of basic coins (BC); * It mints and burns stablecoins (SC) and reserve coins (RC). * It uses its reserves to buy and sell SC keeping its price pegged to a target price. * The fees it charges while doing so are accumulated in its reserves.

Minimal DJed

Definitions for Stablecoins

- The _target price_ of a stablecoin $SC$ pegged by a currency $P$ is $P^t_{SC} = X^P_{BC}BC,$ where $X^P_{BC}$ is the price of 1 $P$ in $BC$. * Djed does not need to be pegged to a fiat currency, it just needs a target price. - The _actual price_ of a stablecoin is $P_C = P^t_{SC}$ if $N_{SC} = 0$ or $P_C = min(P^t_{SC}, \frac{R}{N_{SC}})$ otherwise, where $N_{SC}$ is the number of stablecoins in circulation. This price exists because Djed's reserves may be insufficient to buy back all stablecoins for the target price. - _Liability_ is denoted by $L(N_{SC}) = N_{SC} P_{SC}$ and is the portion of Djed's reserves that would be necessary to buy back all $SC$. - The _reserve ratio_ is $r(R, N_{SC}) = \frac{R}{L(N_{SC})}$ and should be kept high due to $P_{SC}$ instability. - The _minimum reserve ratio_ and _maximum reserve ratio_ are denoted by $r_{min}$ and $r_{max}$, respectively. - The _threshold number of stablecoins_, denoted by $N^*_{SC}$, allows for users to buy reservecoins right after (re)initialization, contributing to the quick growth of the reserve.

Constraints for Stablecoins

- To keep a high reserve ratio, users are forbidden to buy $SC$ and sell $RC$ if $r(R, N_{SC}) < r_{min}$. - To prevent dilution for $RC$ holders, users are forbidden to buy more $RC$ if, before of after the purchase, $r(R, N_{SC}) > r_{max}$ _unless_ $N_{SC} < N^*_{SC}$. - Note that due to price fluctuation, it is still possible for the reserve ratio to rise above $r_{max}$ or go below $r_{min}$.

Definitions for Reservecoins

- _Equity_, or reserve surplus, is $E(R, N_{SC}) = R - L(N_{SC})$. - The _target price_ for RC is $P^t_{RC}(R, N_{SC}, N_{RC}) = \frac{E(R, N_{SC})}{N_{RC}}$, where $N_{RC}$ is the number of reservecoins in circulation. * Note that equity is shared among RC holders. * Note the $P^t_{RC}$ is undefined when $N_{RC} = 0$. * Also note that if $P^t_{RC} = 0$ when $E(R, N_{SC}) = 0$ any amount of reservecoins could be bought at no cost! - The _buying price_ for reservecoins is either $P^b_{RC}(R, N_{SC}, N_{RC}) = max(P^t_{RC}, P^\mu_{RC})$, when $P^t_{RC}$ is defined with $P^\mu_{RC}$ a parameter of Djed, or $P^\mu_{RC}$ otherwise.

### Djed state machine
Actions

| Action | User sends | User receives | Condition | | ------------ | ------------------------------- | ----------------------------- | -------------------------------------------------------------------- | | Buy SC | $n (1 + fee) P_{SC}$ | $n SC$ | $r(R, N_{SC}) \ge r_{min}$ | | Sell SC | $n SC$ | $n (1 - fee) P_{SC}$ | | | Buy RC | $n (1 + fee) P^b_{RC}$ | $n RC$ | $r(R, N_{sc}) \le r_{max}$ or $N_{SC} < N^*_{SC}$ | | Sell RC | $n RC$ | $n (1 - fee) P^t_{RC}$ | $r(R, N_{SC}) \ge r_{min}$ | - Conditions must hold before and after an action.

Parameters and state

- State variables: $R$, $N_{SC}$ and $N_{RC}$. - Parameters : $r_{min}$, $r_{max}$, $fee$, $P^\mu_{SC}$, and $N^*_{SC}$, constrained by: * $r_{min} > 1 + fee$, * $r_{max} \ge r_{min}$, * $0 \le fee \le 1$, * $N^*_{SC} > 0$, * $P^\mu_{RC} > 0$, and, very importantly, * $X^{PC}_{RC} > 0$, otherwise the pegged currency collapses and so does the stablecoin.

Basic elements of Plutus

https://docs.cardano.org/plutus/learn-about-plutus

Offchain and onchain code

EUTXO accounting model

In the Unspent Transaction Output (UTXO) model, a transaction has inputs and outputs, where the inputs are unspent outputs from previous transactions. As soon as an output is used as input in a transaction, it becomes spent and can never be used again. The output is specified by an address (a public key or public key hash) and a value (consisting of an ada amount and optional, additional native token amounts). EUTXO extends the UTXO model by allowing output addresses to contain complex logic to decide which transactions can unlock them, and by adding custom data to all outputs. This model offers unique advantages over other accounting models. The success or failure of transaction validation _depends only on the transaction itself and its inputs_ and not on anything else on the blockchain. Consequently, the validity of a transaction can be checked off-chain before the transaction is sent to the blockchain. A transaction can still fail if some other transaction concurrently consumes an input that the transaction is expecting. However, if all inputs are still present, the transaction is guaranteed to succeed. The EUTXO model extends the UTXO model in two ways: - It generalizes the concept of ‘address’ by using the lock-and-key analogy. Instead of restricting locks to public keys and keys to signatures, _addresses in the EUTXO model can contain arbitrary logic in the form of scripts_. For example, when a node validates a transaction, the node determines whether or not the transaction is allowed to use a certain output as an input. The transaction will look up the script provided by the output's address and will execute the script if the transaction can use the output as an input. - The second difference between UTXO and EUTXO is that outputs can carry (almost) arbitrary data in addition to an address and value. This makes scripts much more powerful by allowing them to carry state information.

Plutus scripts

https://docs.cardano.org/plutus/Plutus-validator-scripts Cardano uses scripts to validate actions. These scripts, which are pieces of code, implement pure functions with True or False outputs. Script validation is the process of invoking the script interpreter to run a given script on appropriate arguments. A script is a program that decides whether or not the transaction that spends the output is authorized to do so. Such a script is called a validator script, because it validates whether the spending is allowed. A simple validator script would check whether the spending transaction was signed by a particular key – this would exactly replicate the behavior of simple pay-to-pubkey outputs. However, with a bit of careful extension, we can use scripts to express useful logic on the chain. The way the EUTXO model works is that validator scripts are passed three arguments: - Datum: this is a piece of data attached to the output that the script is locking (strictly, again, just the hash is present). This is typically used to carry state. - Redeemer: this is a piece of data attached to the spending input. This is typically used to provide an input to the script from the spender. - Context: this is a piece of data that represents information about the spending transaction. This is used to make assertions about the way the output is being sent (such as “Bob signed it”).

Plutus transactions

https://docs.cardano.org/plutus/Plutus-transactions A transaction is a piece of data that contains both inputs and outputs, and as of the Alonzo era, they can also include Plutus scripts. Inputs are unspent outputs from previous transactions (UTxO). Users’ funds are stored as unspent transaction outputs, each of which has a quantity that can be spent. Inputs are unspent outputs from previous transactions. As soon as an UTxO is used as input in a transaction, it becomes spent and can never be used again. The output is specified by: - an address: that contains a payment credential and an optional stake credential, either a public/verification key hash or a script hash. Technically, the stake credential can also be a pointer to the registration certificate. - a value: reflects the actual ada amount that can be spent. An output’s address determines which transactions are allowed to ‘unlock’ the output and use it as an input. A transaction must be signed by the owner of the private key corresponding to the address. In short, inputs contain references to UTXOs introduced by previous transactions, and outputs are the new UTXOs that this transaction will produce. Also, if we think about it, this allows us to change the state of a smart contract since new data can be contained in the produced outputs. This flow-diagram gives a better idea of what the components of a transaction are at a technical level:

Oracles

Oracles that bring off-chain data onto the chain to interact with and feed smart contracts. In addition, oracles create a centralized and trusted off-chain data feed for Plutus applications (for example, to interact with price feeds from various centralized exchanges).

Native tokens

A token is a short term for “asset token”, which is the on-chain representation of an asset and its basic accounting unit. A token can represent one ada, one house, or the value of ten tonnes of coffee, for example. Native tokens represent some value and act as an accounting unit, which can be used for payments, transactions, and can be sent to an exchange address. Native means that these tokens are supported by the Cardano accounting ledger without the need for additional smart contracts, as the ledger features built-in support to track ownership and transfer of more than one type of asset. While both ada and native tokens hold value and act as a payment and transaction unit, only ada is used for fees and rewards, while only native tokens can be customly created.

Minting policies

Minting policies are defined by the users who want to create a new asset. For example, a user might wish to only allow themselves to mint any more of a certain kind of token. This would be specified in the policy. The native token lifecycle consists of five main phases: 1. minting 2. issuing 3. using 4. redeeming 5. burning The following diagram outlines the interaction between the system components: The main groups of actors are: - Asset controllers, who define the policy for the asset class, and authorise token issuers to mint/burn tokens. They may also retain co-signing rights for any tokens that are issued/burnt. - Token issuers, who mint new tokens, maintain the reserve of tokens in circulation, issue them to token holders, and burn tokens when they are no longer of use. - Token holders, who hold tokens, send them to other users, use them for payment, and who may redeem them with the issuers when they have finished using them. Token users may include normal users, exchanges etc.

Cardano implementation of Djed

https://github.com/input-output-hk/stablecoin-plutus/

Main elements

Actions

- Order submission * Funds are locked together with an order description (token and datum). - Aggregate orders * Orders sitting on `REQUEST` contract are aggregated into a single transaction. - Update Djed state * Orders are sorted by timestamp and transaction id. * A new utxo with the new state is produced for `STABLECOIN`. - Provide operator fees * Introduced to palliate against cheating situations regarding operator cheating. * Paid when orders are submitted. - Collect fee * Operator only collects part of his fees at processing time. * Remaining fees are claimed after a deadline if no complaints are filed. Otherwise fees go to Djed reserve.

Important issues

- Successfully submitted orders may become unstable while being processed. * Orders are submitted in batch and then sorted by timestamp and transaction id. This is to avoid manipulation by a Buyer/Seller. Consequently, a successfully submitted order may become unstable as its price depends on Djed' state. - Adaptive price calculation. * Prices depend on Djed' state. * Buying reserve coins. - There should be enough ADA to back a buying order for reserve coins. - Operations on StableCoins. * Do not require adapting price calculation. * Depend only on the exchange rate. - An operator is an untrusted party. * Can ommit orders. * Can depoly a stablecoin contract with a fake currency symbol. - Fees are used to palliate cheating. * Malitious deployments/upgrades can happen. (No current solution for that.)

Contract Stablecoin.hs

Introduction

Contract `stablecoinContract` is the main contract maintaing the Djed bank state and responsible for minting/redeeming stablecoins and reservecoins. ```haskell stableCoinContract :: StableCoinParams -> RequestScriptHash -> RewardFeeScriptHash -> BuiltinData -> BuiltinData -> BuiltinData -> Bool ``` This is a paramterized validator (apart from the standard datum, redeemer and context that a validator always receives) by parameters specific to a stablecoin, the hash of the `REQUEST` script and the hash of `REWARD FEE` script. We focus at first on the case where `Stablecoin`'s redeemer is set to process orders from `REQUEST` contract. When Redeemer = Process, the validator evaluates successfully when the following conditions are satisfied: 1. StableCoin NFT token is present as input 2. scParamsValidity is set to true in previous Djed state 3. No stablecoin/reservecoin minting is performed 4. Transaction is only signed by stablecoin operator 5. First output utxo corresponds to stablecoin script output 6. StableCoin NFT token is present as output 7. utxos of pending orders are expected to be sorted in input (i.e., ordered by timestamp and utxo) such that: a. The new Djed state is updated properly w.r.t., this specific order b. Liquidity sitting at the djed contract = new reserve + minAdaOperator c. stablecoins, reservecoins and redeeming Ada are properly distributed to their respective recipients d. minAdaTransfer is transferred back to submitters e. Reward fees sent back to buyer/seller when corresponding order fails stability constraints f. Number of stablecoins at new djed utxo = MaxDjedMintingToken - scN_SC g. Number of reservecoins at new djed utxo = MaxDjedMintingToken - scN_RC 8. Expected request fees are collected by stablecoin operator 9. Expected reward fees for successful orders are submitted to RewardFee contract (i.e., no submission when all orders are unsuccessful), s.t. a. The last order Id processed is propertly set in the RewardFee state b. The claiming deadline is set to upper limit of txValidRange + scFeeCollectionInterval c. The order minting symbol is properly set 10. Expected number of order tokens is burnt 11. The length of txValidRange = processInterval

Main datatypes

The following datatypes are declared at CustomContext.hs.

CustomSCOrder

[CustomContext.hs#L168](https://github.com/input-output-hk/stablecoin-plutus/blob/f3e702c65139006785a482068da9208fb5273b3d/onchain/Cardano/Djed/CustomContext.hs#L168) Customized order type to allow for partial decoding in validator. ```haskell data CustomSCOrder = CustomSCOrder { scAction :: !BuiltinSCAction , scSubmitter :: !BuiltinAddress , scRate :: !BuiltinRational , scTimeStamp :: !BuiltinPOSIXTime , scOrderSymbol :: !BuiltinCurrencySymbol } deriving (Show, Generic, Haskell.Eq) ```

CustomScriptContext

[CustomContext.hs#L261](https://github.com/input-output-hk/stablecoin-plutus/blob/f3e702c65139006785a482068da9208fb5273b3d/onchain/Cardano/Djed/CustomContext.hs#L261) Customized Script Context. ```haskell data CustomScriptContext = CustomScriptContext { scriptContextTxInfo :: BuiltinTxInfo , scriptContextPurpose :: BuiltinScriptPurpose } deriving (Show, Generic, Haskell.Eq) ```

CustomTxInfo

[CustomContext.hs#L304](https://github.com/input-output-hk/stablecoin-plutus/blob/f3e702c65139006785a482068da9208fb5273b3d/onchain/Cardano/Djed/CustomContext.hs#L304) Customized TxInfo for stablecoin, order minting and oracle contracts. ```haskell data CustomTxInfo = CustomTxInfo { ctxInfoInputs :: BuiltinListTxInInfo , ctxInfoOutputs :: BuiltinListTxOut , ctxInfoMint :: BuiltinValue , ctxInfoValidRange :: BuiltinPOSIXTimeRange , ctxInfoSignatories :: BuiltinListPubKeyHash , ctxInfoData :: BuiltinInfoData } deriving (Show, Generic, Haskell.Eq) ```

Validator definition: stableCoinContract

This contract appears to be responsible for two actions of Djed' statemachine: aggregate orders and update state.

stableCoinContract params@(StableCoinParams {..}) requestHash rewardHash r_state r_redeemer r_ctx =

Syntax StableCoinParams {..} appears to expose scStableCoinCurrencySymbol.

  -- ...
  validDjedMinting && validSignatory &&
  case redeemer of
  -- ...
      StableCoinProcess ->
      ( CC.scParamsValidity o_state ) && validProcessOrder
where

Binding !strictOldState = CC.strictUnsafeFromBuiltin' @CC.CustomBankState r_state is an example of a bang pattern: it behaves by first evaluating the expression on the RHS and then it matches the pattern in the LHS. Essentially, it makes strictOldState, well, strict.

    !strictOldState = CC.strictUnsafeFromBuiltin' @CC.CustomBankState r_state
    !o_state = getResult strictOldState
    !all_inputs = CC.toCustomInfoInputs' ctxInfoInputs
    !(CC.CustomTxInfo {..}) = getResult strictTxInfo      

Syntax CC.CustomTxInfo {..} seems to expose ctxInfoData below, in validProcessOrder. It appears to be a RecordWildCard Haskell language extension.

    scrRef = CC.toSpendingBuiltinTxOutRef' scriptContextPurpose
    !all_outputs = CC.toBuiltinList' ctxInfoOutputs
    !scrHash = retrieveStableCoinHash scStableCoinCurrencySymbol requestHash rewardHash scrRef all_inputs

Function retrieveStableCoinHash (See Core/StableCoin.hs#L929) returns the stablecoin script hash associated with the provided consumed utxo.

Predicate validProcessOrder

See StableCoin.hs#L265.

    validProcessOrder =
      let 

Retrives orders

          !strictOrders = retrieveOrders scOrderMintingSymbol requestHash all_inputs ctxInfoData
          !pendingOrders = getResult strictOrders

Function retrieveOrders (See Core/StableCoin.hs#L956) returns the sorted list of pending orders in input.

Sets transaction range

          txRange = PlutusTx.unsafeFromBuiltinData @POSIXTimeRange ctxInfoValidRange

New bank state and remaining utxos

Variable new_state comes from the context information: CustomScriptContext.scriptContextTxInfo -> CustomTxInfo.ctxInfoData. Variable tail_outputs holds the utxos that also come from the context information: CustomScriptContext.scriptContextTxInfo -> CustomTxInfo.ctxInfoOutputs).

          !(new_state, tail_outputs) = validScriptOutput (getResult scrHash)

Function validScriptOutput (See StableCoin.hs#L238) is not a predicate: it produces a pair (CC.CustomBankState, [BuiltinData]).

Function scMinAdaTransfer

          minAdaTransfer = CC.scMinAdaTransfer new_state

scMinAdaTransfer (See CustomContext.hs#L93) is a constructor of CustomBankState.

Function toComputeReserve

          c_state = toComputeReserve o_state

Function toComputeReserve (See Core/StableCoin.hs#L408) is a cohercion function CustomBankState -> ComputeReserve, where o_state is the old state, retrieved from r_state parameter.

Variable oldOrderId

          oldOrderId = PlutusTx.unsafeFromBuiltinData (CC.scLastOrder o_state)

Function unsafeFromBuiltinData :: BuiltinData -> a belongs to class UnsafeFromData (See PlutusTx/IsData/Class.hs#L43). Converts a value from BuiltinData, calling error if this fails.

Function processOrders

          !(SCOnChainResult c_state' dest_l totalRwdFees lastOrder) =
            processOrders params minAdaTransfer oldOrderId pendingOrders c_state

Function processOrders (See Core/StableCoin.hs#L866), with type

processOrders :: StableCoinParams ->  MinAdaTransfer ->  (Maybe OrderId) ->
                            [NormalizedOrder] ->  ComputeReserve -> SCOnChainResult

processes each order sequentially and updates the state only for successful ones. Returns an SCResult instance, which contains:

Function updateCustomState

          !p_state = updateCustomState c_state' o_state

Function updateCustomState (See Core/StableCoin.hs#L415) does what is expected of it.

Variable rwdClaimingDeadline

          !rwdClaimingDeadline =
            validRecipientsAndRewardFees scStableCoinCurrencySymbol
            scStableCoinTokenName scReserveCoinTokenName rewardHash lastOrder
            totalRwdFees ctxInfoData dest_l tail_outputs

Function validRecipientsAndRewardFees(See Core/StableCoin.hs#L995) has the following type.

validRecipientsAndRewardFees :: StableCoinCurrencySymbol ->  TokenName ->  TokenName ->
  RewardFeeScriptHash -> Maybe OrderId -> Integer ->
  CC.BuiltinInfoData -> [SCOnChainDestination] -> [CC.BuiltinTxOut] -> POSIXTime

Function validProcessState

      in
        debug "stableCoinContract: Invalid Djed state after processing !!!"
        ( validProcessingState p_state new_state lastOrder ) &&

Function validProcessingState (See Core/StableCoin.hs#L1157) returns true when commonStateEquality (See Core/StableCoin.hs#L1098) -- it checks if two Bank States are equal) is true and scReserve, scParamsValidity and scScriptTxOutRef are the same for both states. Note that conditions scMinAdaTransfer[new] > 0 and scMinAdaOperator[new] > 0.

Constraint over scOrderMintingSymbol

        -- exact number of order token to be burnt is handled by order minting contract
        debug "stableCoinContract: Invalid burning of order token !!!"
        ( CC.builtinValueOf' scOrderMintingSymbol djedOrderToken ctxInfoMint < 0 ) &&

Function builtinValueOf' (See CustomContext.hs#L602) performs partial decoding of the value map (ctxInfoMint) w.r.t. the currency symbol (scOrderMintingSymbol) and token name (djedOrderToken) to be searched for:

Function validProcessTxRange

        -- valid process interval, last order timestamp expired and claiming deadline properly set
        ( validProcessTxRange txRange lastOrder rwdClaimingDeadline scFeeCollectionInterval )

Function validProcessTxRange (See Core/StableCoin.hs#L1217) returns true when the following conditions are satisfied:

It raises an error if: