Changes after review: add F5 invariant

ajna-finance · Apr 20, 2023 · 1b21017 · 1b21017
1 parent 74b255f
commit 1b21017
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 0 deletions.
diff --git a/src/base/Pool.sol b/src/base/Pool.sol
@@ -771,6 +771,11 @@ abstract contract Pool is Clone, ReentrancyGuard, Multicall, IPool {
  return PoolCommons.utilization(emaState);
  }
 
+ /// @inheritdoc IPoolDerivedState
+ function depositScale(uint256 index_) external view override returns (uint256) {
+ return deposits.scaling[index_];
+ }
+
  /// @inheritdoc IPoolState
  function emasInfo() external view override returns (uint256, uint256, uint256, uint256) {
  return (

diff --git a/src/interfaces/pool/commons/IPoolDerivedState.sol b/src/interfaces/pool/commons/IPoolDerivedState.sol
@@ -41,4 +41,13 @@ interface IPoolDerivedState {
  */
  function depositUtilization() external view returns (uint256);
 
+ /**
+ * @notice Returns the scaling value of deposit at given index.
+ * @param index_ Deposit index.
+ * @return Deposit scaling.
+ */
+ function depositScale(
+ uint256 index_
+ ) external view returns (uint256);
+
 }
diff --git a/tests/INVARIANTS.md b/tests/INVARIANTS.md
@@ -49,6 +49,7 @@
 - **F2**: For any index `i`, the prefix sum up to and including `i` is the sum of values stored in indices `j<=i`
 - **F3**: For any index `i < MAX_FENWICK_INDEX`, `findIndexOfSum(prefixSum(i)) > i`
 - **F4**: For any index i, there is zero deposit above i and below findIndexOfSum(prefixSum(i) + 1): `depositAtIndex(j) == 0 for i < j < findIndexOfSum(prefixSum(i)+1)`
+- **F5**: Global scalar is never updated (`DepositsState.scaling[8192]` is always 0)
 
 ## Exchange rate invariants ##
 - **R1**: Exchange rates are unchanged by pledging collateral

diff --git a/tests/forge/invariants/base/BasicInvariants.t.sol b/tests/forge/invariants/base/BasicInvariants.t.sol
@@ -43,6 +43,7 @@ abstract contract BasicInvariants is BaseInvariants {
  * F2: For any index i, the prefix sum up to and including i is the sum of values stored in indices j<=i
  * F3: For any index i < MAX_FENWICK_INDEX, findIndexOfSum(prefixSum(i)) > i
  * F4: For any index i, there is zero deposit above i and below findIndexOfSum(prefixSum(i) + 1): findIndexOfSum(prefixSum(i)) == findIndexOfSum(prefixSum(j) - deposits.valueAt(j)), where j is the next index from i with deposits != 0
+ * F5: Global scalar is never updated (`DepositsState.values[8192]` is always 0)
  ****************************************************************************************************************************************/
 
  // checks pool lps are equal to sum of all lender lps in a bucket 
@@ -352,6 +353,11 @@ abstract contract BasicInvariants is BaseInvariants {
  }
  }
 
+ // **F5**: Global scalar is never updated (`DepositsState.scaling[8192]` is always 0)
+ function invariant_fenwick_globalscalar_F5() public useCurrentTimestamp {
+ require(_pool.depositScale(8192) == 0, "F5: Global scalar was updated");
+ }
+
  function invariant_call_summary() public virtual useCurrentTimestamp {
  console.log("\nCall Summary\n");
  console.log("--Lender----------");