Ideas of Properties and Invariants

[henry-hz]

When analyzing the given smart contract code for a perpetual trading platform, it is essential to identify and establish the properties and invariants that must hold to ensure the contract operates securely and as expected. Here are some key properties and invariants to consider:

General Properties and Invariants

1. Governance Control:

   • The gov address should always be a valid address.
   • Only the gov can update the gov address or link contracts.

2. Contract Linking:

   • chainlink, pool, and store should always be linked before performing any trading operations.

3. Balance Management:

   • Users should not be able to withdraw more than their balance.
   • Balance increments and decrements should correctly reflect deposits, withdrawals, and trading fees.

4. Margin and Leverage:

   • Users' equity should always be sufficient to cover their locked margin.
   • Ensure leverage constraints are respected when opening positions.

5. Order and Position Management:

   • Orders should only be executable if they meet specified conditions regarding market price and order type.
   • Ensure positions are properly updated or removed when orders are executed or canceled.

6. Funding Rates and PnL Calculation:

   • Funding rates should be calculated and updated correctly based on open interest.
   • PnL (Profit and Loss) should be calculated accurately based on current prices and funding fees.

Specific Invariants

Governance

1. Governance Updates:

   require(_gov != address(0), "!address");

   • Ensure new gov address is not zero.

2. Contract Linking:

   function link(address _chainlink, address _pool, address _store) external onlyGov {
      require(_chainlink != address(0) && _pool != address(0) && _store != address(0), "!address");
      // ... rest of the code
   }

Deposit and Withdrawals

3. Deposit:

   require(amount > 0, "!amount");

   • Ensure deposit amount is greater than zero.

4. Withdrawal:

   • Ensure the amount to withdraw does not exceed the user's balance.
   • Ensure equity after withdrawal is not less than the locked margin:

     require(int256(lockedMargin) <= int256(balance - amount) + upl, "!equity");

Order Handling

5. Submit Order:

   require(market.maxLeverage > 0, "!market");
   require(int256(lockedMargin) <= equity, "!equity");
   require(params.margin > 0 && int256(lockedMargin + params.margin) <= equity, "!margin");
   require(market.minSize <= params.size, "!min-size");
   require(chainlinkPrice > 0, "!chainlink");

   • Ensure market is valid, equity is sufficient, and order size and price are within valid ranges.

6. Order Execution:

   • Ensure order conditions are met based on current market prices before execution.

     if (
     order.orderType == 0 || order.orderType == 1 && order.isLong && chainlinkPrice <= order.price
        || order.orderType == 1 && !order.isLong && chainlinkPrice >= order.price
        || order.orderType == 2 && order.isLong && chainlinkPrice >= order.price
        || order.orderType == 2 && !order.isLong && chainlinkPrice <= order.price
     ) {
     // Order can be executed
     }

Position Management

7. Increase Position:

   require(position.size == 0 || order.isLong == position.isLong, "!direction");

   • Ensure new positions are only added if they are in the same direction or if it's a new position.

8. Decrease Position:

   • Ensure positions are decreased correctly, and PnL and funding fees are accounted for:

     (int256 pnl, int256 fundingFee) = _getPnL(order.market, position.isLong, price, position.price, executedOrderSize, position.fundingTracker);

Liquidation

9. Liquidation:
   • Ensure users are liquidated only if their margin level is below the minimum required margin level.

     if (marginLevel < store.minimumMarginLevel()) {
     // User is eligible for liquidation
     }

By formalizing these properties and invariants, you can apply formal verification methods to analyze the smart contract and ensure that it behaves as expected under all possible scenarios. This can help identify and prevent potential bugs and vulnerabilities, leading to a more secure and robust trading platform.