[WIP]: fix: Liquidity growth calculation in fees logic & fee cache in storage

.prettierignore

@@ -6,3 +6,4 @@ snapshots
 report
 src/dependencies
 tests/mocks/JsonBindings.sol
+.certora_internal/

certora/conf/HubAccrueSupplyRate.conf

@@ -5,22 +5,18 @@
 		"certora/harness/MathWrapper.sol"
 	],
 	"loop_iter": 3,
-	"msg": "HubAccrue supply rate",
+	"msg": "only fee diff",
 	"multi_assert_check": true,
 	"optimistic_loop": true,
 	"parametric_contracts": [
 		"HubHarness"
 	],
 	"prover_args": [
-		"-splitParallel",
-		"true",
-		"-dontStopAtFirstSplitTimeout",
-		"true"
+		" -destructiveOptimizations twostage -s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]"
 	],
 	"rule": [
-		"unrealizedFeeSharesSupplyRate"
+		"previewRemoveByShares_time_monotonic"
 	],
-	// no need for sanity check as the rule ends in a satisfy command	
 	"rule_sanity": "none",
 	"smt_timeout": 7200,
 	"solc_via_ir": true,

certora/harness/HubHarness.sol

@@ -14,7 +14,7 @@ contract HubHarness is Hub {
   function accrueInterest(uint256 assetId) external {
     Asset storage asset = _assets[assetId];
 
-    asset.accrue(_spokes, assetId);
+    asset.accrue();
   }
 
   function toSharesDown(
@@ -55,6 +55,6 @@ contract HubHarness is Hub {
 
   function unrealizedFeeShares(uint256 assetId) external view returns (uint256) {
     Asset storage asset = _assets[assetId];
-    return asset.unrealizedFeeShares();
+    return asset.feeShares;
   }
 }

certora/spec/HubAccrueSupplyRate.spec

@@ -79,3 +79,39 @@ rule unrealizedFeeSharesSupplyRate(uint256 assetId){
 
 }
 
+rule previewRemoveByShares_time_monotonic(uint256 assetId, uint256 shares){
+    env e1; env e2; env e3;
+    uint256 oneM = 1000000;
+    require e1.block.timestamp < e2.block.timestamp && e2.block.timestamp < e3.block.timestamp;
+
+    require hub._assets[assetId].lastUpdateTimestamp!=0 && hub._assets[assetId].lastUpdateTimestamp == e1.block.timestamp; 
+
+    //correlate the drawn index with the symbolic one, assume increasing and min value as proved in
+    // HubAccrueIntegrityDrawnIndex.spec
+    require hub._assets[assetId].drawnIndex == symbolicDrawnIndex(e1.block.timestamp);
+    //based on rule drawnIndex_increasing(assetId);
+    require  symbolicDrawnIndex(e1.block.timestamp) <= symbolicDrawnIndex(e2.block.timestamp);
+    require  symbolicDrawnIndex(e2.block.timestamp) <= symbolicDrawnIndex(e3.block.timestamp);
+    //based on requireInvariant baseDebtIndexMin(assetId); 
+    require  symbolicDrawnIndex(e1.block.timestamp) >= wadRayMath.RAY();
+    require  symbolicDrawnIndex(e3.block.timestamp) <= wadRayMath.RAY() * 2;
+
+
+    mathint assets_e1 = getAddedAssets(e1, assetId);
+    mathint shares_e1 = hub._assets[assetId].addedShares;
+    //requireInvariant totalAssetsVsShares(assetId,e);
+    require assets_e1 >= shares_e1 ;
+
+    // get the fee shares and asset at e2
+    uint256 feeShares_e2 = unrealizedFeeShares(e2,assetId);
+    mathint assets_e2 = getAddedAssets(e2, assetId);
+    mathint shares_e2 = getAddedShares(e2, assetId);
+
+    // get the fee shares and asset at e2
+    uint256 feeShares_e3 = unrealizedFeeShares(e3,assetId);
+    mathint assets_e3 = getAddedAssets(e3, assetId);
+    mathint shares_e3 = getAddedShares(e3, assetId);
+    assert feeShares_e2 <= feeShares_e3;
+
+    assert (assets_e3 + oneM) * (shares_e2 + oneM) >= (assets_e2 + oneM) * (shares_e3 + oneM); 
+}

snapshots/Hub.Operations.json

@@ -1,14 +1,14 @@
 {
-  "add": "113832",
-  "draw": "122026",
-  "eliminateDeficit: full": "57818",
-  "eliminateDeficit: partial": "67394",
-  "payFee": "73744",
-  "refreshPremium": "96823",
-  "remove: full": "75059",
-  "remove: partial": "80306",
-  "reportDeficit": "118722",
-  "restore: full": "97460",
-  "restore: partial": "110890",
-  "transferShares": "79425"
+  "add": "113922",
+  "draw": "122579",
+  "eliminateDeficit: full": "57911",
+  "eliminateDeficit: partial": "67487",
+  "payFee": "69276",
+  "refreshPremium": "96807",
+  "remove: full": "75842",
+  "remove: partial": "80511",
+  "reportDeficit": "109460",
+  "restore: full": "90998",
+  "restore: partial": "104428",
+  "transferShares": "70166"
 }

snapshots/Spoke.Getters.json

@@ -1,7 +1,7 @@
 {
   "getUserAccountData: supplies: 0, borrows: 0": "12164",
-  "getUserAccountData: supplies: 1, borrows: 0": "47260",
-  "getUserAccountData: supplies: 2, borrows: 0": "77471",
-  "getUserAccountData: supplies: 2, borrows: 1": "98212",
-  "getUserAccountData: supplies: 2, borrows: 2": "117607"
+  "getUserAccountData: supplies: 1, borrows: 0": "49375",
+  "getUserAccountData: supplies: 2, borrows: 0": "81701",
+  "getUserAccountData: supplies: 2, borrows: 1": "102442",
+  "getUserAccountData: supplies: 2, borrows: 2": "121837"
 }

snapshots/Spoke.Operations.ZeroRiskPremium.json

@@ -1,32 +1,32 @@
 {
-  "borrow: first": "198976",
-  "borrow: second action, same reserve": "179497",
-  "liquidationCall: full": "291027",
-  "liquidationCall: partial": "315121",
-  "permitReserve + repay (multicall)": "235530",
-  "permitReserve + supply (multicall)": "140910",
-  "permitReserve + supply + enable collateral (multicall)": "176141",
-  "repay: full": "151572",
-  "repay: partial": "176035",
+  "borrow: first": "194629",
+  "borrow: second action, same reserve": "175150",
+  "liquidationCall: full": "291636",
+  "liquidationCall: partial": "309871",
+  "permitReserve + repay (multicall)": "231183",
+  "permitReserve + supply (multicall)": "141000",
+  "permitReserve + supply + enable collateral (multicall)": "176809",
+  "repay: full": "153662",
+  "repay: partial": "178125",
   "setUserPositionManagerWithSig: disable": "44918",
   "setUserPositionManagerWithSig: enable": "68947",
-  "supply + enable collateral (multicall)": "154083",
-  "supply: 0 borrows, collateral disabled": "115722",
-  "supply: 0 borrows, collateral enabled": "120119",
-  "supply: 1 borrow": "120111",
-  "supply: second action, same reserve": "103019",
+  "supply + enable collateral (multicall)": "154751",
+  "supply: 0 borrows, collateral disabled": "115812",
+  "supply: 0 borrows, collateral enabled": "120787",
+  "supply: 1 borrow": "120779",
+  "supply: second action, same reserve": "103687",
   "updateUserDynamicConfig: 1 collateral": "73761",
   "updateUserDynamicConfig: 2 collaterals": "88621",
-  "updateUserRiskPremium: 1 borrow": "95282",
-  "updateUserRiskPremium: 2 borrows": "111374",
+  "updateUserRiskPremium: 1 borrow": "97397",
+  "updateUserRiskPremium: 2 borrows": "110694",
   "usingAsCollateral: 0 borrows, enable": "58976",
-  "usingAsCollateral: 1 borrow, disable": "105529",
+  "usingAsCollateral: 1 borrow, disable": "107644",
   "usingAsCollateral: 1 borrow, enable": "32298",
-  "usingAsCollateral: 2 borrows, disable": "127994",
+  "usingAsCollateral: 2 borrows, disable": "130109",
   "usingAsCollateral: 2 borrows, enable": "41876",
-  "withdraw: 0 borrows, full": "127680",
-  "withdraw: 0 borrows, partial": "132727",
-  "withdraw: 1 borrow, partial": "161709",
-  "withdraw: 2 borrows, partial": "184162",
-  "withdraw: non collateral": "126789"
+  "withdraw: 0 borrows, full": "128578",
+  "withdraw: 0 borrows, partial": "133162",
+  "withdraw: 1 borrow, partial": "162722",
+  "withdraw: 2 borrows, partial": "185175",
+  "withdraw: non collateral": "117877"
 }

snapshots/Spoke.Operations.json

@@ -1,32 +1,32 @@
 {
-  "borrow: first": "269145",
-  "borrow: second action, same reserve": "212666",
-  "liquidationCall: full": "324413",
-  "liquidationCall: partial": "348507",
-  "permitReserve + repay (multicall)": "268909",
-  "permitReserve + supply (multicall)": "140910",
-  "permitReserve + supply + enable collateral (multicall)": "176141",
-  "repay: full": "146213",
-  "repay: partial": "209414",
+  "borrow: first": "264782",
+  "borrow: second action, same reserve": "208303",
+  "liquidationCall: full": "325006",
+  "liquidationCall: partial": "343241",
+  "permitReserve + repay (multicall)": "264546",
+  "permitReserve + supply (multicall)": "141000",
+  "permitReserve + supply + enable collateral (multicall)": "176809",
+  "repay: full": "148303",
+  "repay: partial": "211488",
   "setUserPositionManagerWithSig: disable": "44918",
   "setUserPositionManagerWithSig: enable": "68947",
-  "supply + enable collateral (multicall)": "154083",
-  "supply: 0 borrows, collateral disabled": "115722",
-  "supply: 0 borrows, collateral enabled": "120119",
-  "supply: 1 borrow": "120111",
-  "supply: second action, same reserve": "103019",
+  "supply + enable collateral (multicall)": "154751",
+  "supply: 0 borrows, collateral disabled": "115812",
+  "supply: 0 borrows, collateral enabled": "120787",
+  "supply: 1 borrow": "120779",
+  "supply: second action, same reserve": "103687",
   "updateUserDynamicConfig: 1 collateral": "73761",
   "updateUserDynamicConfig: 2 collaterals": "88621",
-  "updateUserRiskPremium: 1 borrow": "177369",
-  "updateUserRiskPremium: 2 borrows": "262734",
+  "updateUserRiskPremium: 1 borrow": "170231",
+  "updateUserRiskPremium: 2 borrows": "241548",
   "usingAsCollateral: 0 borrows, enable": "58976",
-  "usingAsCollateral: 1 borrow, disable": "187616",
+  "usingAsCollateral: 1 borrow, disable": "180478",
   "usingAsCollateral: 1 borrow, enable": "32298",
-  "usingAsCollateral: 2 borrows, disable": "287353",
+  "usingAsCollateral: 2 borrows, disable": "270962",
   "usingAsCollateral: 2 borrows, enable": "41876",
-  "withdraw: 0 borrows, full": "127680",
-  "withdraw: 0 borrows, partial": "132727",
-  "withdraw: 1 borrow, partial": "241296",
-  "withdraw: 2 borrows, partial": "341022",
-  "withdraw: non collateral": "126789"
+  "withdraw: 0 borrows, full": "128578",
+  "withdraw: 0 borrows, partial": "133162",
+  "withdraw: 1 borrow, partial": "233056",
+  "withdraw: 2 borrows, partial": "323529",
+  "withdraw: non collateral": "117877"
 }