Proposal for additional verification specs

[daejunpark]

In addition to the existing specs, the following specs could also be considered. If the prover is incapable of verifying them, fuzzing could be considered as an alternative.

1. [Share Price Preservation]: For any tx: the share price, totalAssets() / totalSupply(), does not decrease.

   • That is, the price immediately before the tx must be less than or equal to the price immediately after the tx.
   • Note: this spec ensures the correctness of accounting logic, e.g., interest and fees are accurately accounted for, the share price is properly updated prior to converting asset amounts to/from shares, etc.

2. [ERC4626]: The ERC4626 properties, especially the round-trip properties, hold.

3. [Consistency of lastTotalAssets]: After any tx: lastTotalAssets == totalAssets()

   • Small discrepancies may exist due to rounding errors.

4. [Soft Supply Cap]: For any tx, for any market: if the supply increases, then it must not exceed the supply cap.

   • Note: the supply cap may be updated to be below the current supply, thus the supply may exceed the cap temporarily. However, it is not allowed to add further supply once it exceeds the cap. Moreover, the excessive supply may be partially withdrawn, where the remaining supply may still exceed the cap.

5. [Consistency between supplyQueue and withdrawQueue]: If "set(supplyQueue) - set(withdrawQueue)" is non-emtpy, then their cap is zero, with no pending cap.

   • Note: ideally, supplyQueue should be a subset of withdrawQueue. However, a market may be removed from withdrawQueue without updating supplyQueue. That's why certain markets may appear only in supplyQueue. However, the supply cap of such markets must be zero, because of the condition for removal from withdrawQueue.

6. [Consistency of withdrawQueue]: A market whose cap > 0 must be included in the withdraw queue.

   • Note: this is the converse of the existing spec inWithdrawQueueIsEnabled.

7. [Consistency of Market Config]: For any market config:

   • If it's not enabled, then cap == 0 (although a pending cap may exist). That is, if cap > 0, then it's enabled.
     • Note: this has been captured by the existing spec supplyCapIsEnabled.
   • If removableAt > 0, then cap == 0 (with no pending), and it's enabled.
     • Note: this has been partially captured by the existing specs supplyCapIsNotMarkedForRemoval and pendingCapIsNotMarkedForRemoval. To fully capture, an additional spec is needed: !config.enabled => config.removableAt == 0;.

[QGarchery]

Thanks a lot for the ideas ! Here are some thoughts about them:

1. The share price could decrease if there is some bad debt on some market. So to capture your idea where you compare with the price immediately before the tx, we could do a dummy transaction first but then it wouldn't account for interest and fees
2. Good point, this seems like a hard property to prove but a nice one. We have had some troubles with the math operations in the past on metamorpho
3. Same, tough to specify that cleanly too. How do you account for those small rounding errors in the spec ?
4. Thought about this one, and it is in Formal verification wish list #333. I found some exceptions (donations and interest accrual) which makes it a bit difficult to specify it
5. I think it's already covered because any market that is not in the withdraw queue is not enabled (rule enabledIsInWithdrawQueue) and every market that is not enabled has 0 cap (invariant supplyCapIsEnabled)
6. I think it's covered by the rule enabledIsInWithdrawQueue
7. Nice catch !

[QGarchery]

Closing this as 4-7 have been completed, 3 is dropped because it seems difficult to specify, and 1 & 2 have been added to #333