Fix outdates previous hacks (GTM-2353)

assertions-book/previous-hacks/abracadabra-gmx-v2-exploit.mdx

@@ -56,8 +56,8 @@ contract AbracadabraGmxV2Assertion is Assertion {
 
     function triggers() public view override {
         // Trigger on any call to sendValueInCollateral
-        triggerRecorder.registerCallTrigger(
-            this.assertPhantomCollateral.selector, 
+        registerCallTrigger(
+            this.assertPhantomCollateral.selector,
             IGmxV2CauldronRouterOrder.sendValueInCollateral.selector
         );
     }

assertions-book/previous-hacks/abracadabra-hack-3.mdx

@@ -72,7 +72,7 @@ contract AbracadabraCookSolvencyAssertion is Assertion {
     uint256 constant COLLATERIZATION_RATE_PRECISION = 1e5;
 
     function triggers() public view override {
-        triggerRecorder.registerCallTrigger(
+        registerCallTrigger(
             this.assertUserSolvency.selector,
             ICauldronV4.cook.selector
         );

assertions-book/previous-hacks/abracadabra-rounding-error.mdx

@@ -37,12 +37,36 @@ The vulnerability stems from an intricate implementation of a RebaseToken mechan
 
 ## Proposed Solution
 
-Assuming the original implementation was well-intentioned but flawed, a simple invariant check could have prevented the attack:
+Assuming the original implementation was well-intentioned but flawed, a simple invariant check could have prevented the attack.
+
+The key invariant is: **when no assets are owed (elastic = 0), there should be no debt shares (base = 0)**.
 
 ```solidity
-function assertionNoDebtSharesIfNoDebt() public view {
-    if (elastic == 0) {
-        require(base == 0, "No debt shares if no debt");
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.28;
+
+import {Assertion} from "credible-std/Assertion.sol";
+
+interface ICauldronV4 {
+    function totalBorrow() external view returns (uint128 elastic, uint128 base);
+}
+
+contract AbracadabraRebaseInvariantAssertion is Assertion {
+    function triggers() external view override {
+        // Trigger on any storage change to the cauldron
+        registerStorageChangeTrigger(this.assertionNoDebtSharesIfNoDebt.selector);
+    }
+
+    function assertionNoDebtSharesIfNoDebt() external view {
+        ICauldronV4 cauldron = ICauldronV4(ph.getAssertionAdopter());
+
+        ph.forkPostTx();
+        (uint128 elastic, uint128 base) = cauldron.totalBorrow();
+
+        // Core invariant: if no debt exists, no shares should exist
+        if (elastic == 0) {
+            require(base == 0, "No debt shares should exist when no debt");
+        }
     }
 }
 ```

assertions-book/previous-hacks/bybit-safe-ui.mdx

@@ -85,7 +85,7 @@ contract SafeAssertion is Assertion {
 
     // Define the triggers for the assertions
     function triggers() public view override {
-        triggerRecorder.registerStateChangeTrigger(this.implementationAddressChange.selector, 0x0);
+        registerStorageChangeTrigger(this.implementationAddressChange.selector, bytes32(0x0));
     }
 
     function implementationAddressChange() external view {

assertions-book/previous-hacks/compound-upgrade-bug.mdx

@@ -29,26 +29,33 @@ This way even if a bug is introduced, it will be caught by the assertion.
 
 The assertion below calculates the maximum possible rate of COMP accrual and checks that a distribution does not exceed this rate.
 
+<Warning>
+The code below is **conceptual pseudo code** to illustrate the invariant that should be enforced. It uses simplified syntax for accessing storage mappings (`compound.compAccrued[supplier]`) that would not compile in actual Solidity. A real implementation would need to use proper getter functions or storage slot calculations via `ph.load()`.
+</Warning>
+
 ```solidity
-// Verify that COMP accrual never exceeds the maximum possible rate
-function assertionValidCompAccrual() external {
-    PhEvm.CallInputs[] memory distributions = ph.getCallInputs(address(compound), Comptroller.distributeSupplierComp.selector);
+// CONCEPTUAL - Verify that COMP accrual never exceeds the maximum possible rate
+function assertionValidCompAccrual() external view {
+    PhEvm.CallInputs[] memory distributions = ph.getCallInputs(
+        address(comptroller),
+        Comptroller.distributeSupplierComp.selector
+    );
 
     for (uint256 i = 0; i < distributions.length; i++) {
-        bytes memory data = distributions[i].input;
-        (address cToken, address supplier) = abi.decode(stripSelector(data), (address, address));
-
-        // Check COMP accrued before and after distribution
-        ph.forkPreCallState();
-        uint256 preAccrued = compound.compAccrued[supplier];
-        CompMarketState storage supplyState = comptroller.compSupplyState[cToken];
-        uint supplyIndex = supplyState.index;
-        uint maxDeltaPerToken = sub_(supplyIndex, comptroller.compInitialIndex);
-        uint supplierTokens = CToken(cToken).balanceOf(supplier);
-        uint maxIncrease = mul_(supplierTokens, maxDeltaPerToken);
-
-        ph.forkPostCallState();
-        uint256 postAccrued = compound.compAccrued[supplier];
+        // Decode call inputs (selector already stripped by cheatcode)
+        (address cToken, address supplier) = abi.decode(distributions[i].input, (address, address));
+
+        // Check COMP accrued before distribution
+        ph.forkPreCall(distributions[i].id);
+        uint256 preAccrued = comptroller.compAccrued(supplier);
+        uint256 supplyIndex = comptroller.compSupplyState(cToken).index;
+        uint256 maxDeltaPerToken = supplyIndex - comptroller.compInitialIndex();
+        uint256 supplierTokens = CToken(cToken).balanceOf(supplier);
+        uint256 maxIncrease = supplierTokens * maxDeltaPerToken;
+
+        // Check COMP accrued after distribution
+        ph.forkPostCall(distributions[i].id);
+        uint256 postAccrued = comptroller.compAccrued(supplier);
 
         if (postAccrued > preAccrued) {
             uint256 increase = postAccrued - preAccrued;

assertions-book/previous-hacks/cream-finance-2.mdx

@@ -19,51 +19,74 @@ One possible solution is to check price deviations from touched assets in the pr
 This would avoid flashloan price manipulation attacks.
 
 ```solidity
-function assertion_priceDeviation() public view {
-    PhEvm.Logs[] memory logs = PhEvm.getLogs();
-    bytes32[] memory topics = [
-        CTokenInterface.Redeem.selector,
-        CTokenInterface.Borrow.selector,
-        CTokenInterface.RepayBorrow.selector,
-        CTokenInterface.LiquidateBorrow.selector
-    ];
+uint256 constant MAX_DEVIATION_BPS = 500; // 5% max deviation
 
+function assertion_priceDeviation() external view {
+    // Get pre-transaction prices first
+    ph.forkPreTx();
+    PhEvm.Log[] memory logs = ph.getLogs();
 
-    address[] memory touchedAssets = new address[];
+    // Count relevant logs to size our array
+    uint256 count = 0;
     for (uint256 i = 0; i < logs.length; i++) {
-
-        if(logs[i].topics[0] == CTokenInterface.Mint.selector) {
-            touchedAssets.push(getAssetFromMintLog(logs[i]));
-            continue;
-        }
-        if(logs[i].topics[0] == CTokenInterface.Redeem.selector) {
-            touchedAssets.push(getAssetFromRedeemLog(logs[i]));
-            continue;
+        bytes32 topic = logs[i].topics[0];
+        if (topic == CTokenInterface.Mint.selector ||
+            topic == CTokenInterface.Redeem.selector ||
+            topic == CTokenInterface.Borrow.selector ||
+            topic == CTokenInterface.RepayBorrow.selector) {
+            count++;
         }
-        if(logs[i].topics[0] == CTokenInterface.Borrow.selector) {
-            touchedAssets.push(getAssetFromBorrowLog(logs[i]));
-            continue;
-        }
-        if(logs[i].topics[0] == CTokenInterface.RepayBorrow.selector) {
-            touchedAssets.push(getAssetFromRepayBorrowLog(logs[i]));
+    }
+
+    // Collect touched assets and their pre-prices
+    address[] memory touchedAssets = new address[](count);
+    uint256[] memory prePrices = new uint256[](count);
+    uint256 idx = 0;
+
+    for (uint256 i = 0; i < logs.length; i++) {
+        bytes32 topic = logs[i].topics[0];
+        address asset;
+
+        if (topic == CTokenInterface.Mint.selector) {
+            asset = getAssetFromLog(logs[i]);
+        } else if (topic == CTokenInterface.Redeem.selector) {
+            asset = getAssetFromLog(logs[i]);
+        } else if (topic == CTokenInterface.Borrow.selector) {
+            asset = getAssetFromLog(logs[i]);
+        } else if (topic == CTokenInterface.RepayBorrow.selector) {
+            asset = getAssetFromLog(logs[i]);
+        } else {
             continue;
         }
 
+        touchedAssets[idx] = asset;
+        prePrices[idx] = priceOracle.getPrice(asset);
+        idx++;
     }
 
-    uint256[] memory postPrices = new uint256[](touchedAssets);
+    // Get post-transaction prices and compare
+    ph.forkPostTx();
+
     for (uint256 i = 0; i < touchedAssets.length; i++) {
-        postPrices.push(priceOracle.getPrice(touchedAssets[i]));
-    }
+        uint256 postPrice = priceOracle.getPrice(touchedAssets[i]);
+        uint256 prePrice = prePrices[i];
 
-    ph.forkPreTx();
+        // Check deviation in both directions
+        uint256 deviation;
+        if (postPrice > prePrice) {
+            deviation = ((postPrice - prePrice) * 10000) / prePrice;
+        } else {
+            deviation = ((prePrice - postPrice) * 10000) / prePrice;
+        }
 
-    for (uint256 i = 0; i < touchedAssets.length; i++) {
-        uint256 prePrice = priceOracle.getPrice(touchedAssets[i]);
-        require(
-            postPrice[i] < prePrice * (1 + MAX_DEVIATION_FACTOR) &&
-            postPrice[i] > prePrice * (1 - MAX_DEVIATION_FACTOR),
-            "Price deviation too high"
-            );
+        require(deviation <= MAX_DEVIATION_BPS, "Price deviation too high");
+    }
+}
+
+// Helper to extract asset address from log (implementation depends on log structure)
+function getAssetFromLog(PhEvm.Log memory log) internal pure returns (address) {
+    // Decode asset address from log topics or data
+    // Implementation depends on the specific event structure
+    return abi.decode(log.data, (address));
 }
 ```

assertions-book/previous-hacks/euler-finance-donation-hack.mdx

@@ -59,25 +59,30 @@ Attack was carried out for several different assets, including DAI, WETH, and US
 Proper health checks should be performed on the account that is performing the donation.
 It is worth noting that the below assertion checks for modifications made by the user in the transaction.
 The user should never be allowed to make changes to their own collateral or debt that brings their positions under water.
-Assuming we can check run assertions on each call in the transaction and that we can get all modified accounts in the transaction, we can implement the following assertion:
+
+<Warning>
+The code below is **conceptual pseudo code** to illustrate the invariant that should be enforced. The `getModifiedAccounts()` cheatcode does not currently exist. In practice, you would need to identify affected accounts through other means, such as parsing logs with `getLogs()` or tracking call inputs with `getCallInputs()`.
+</Warning>
 
 ```solidity
-function assertionNoUnsafeDebt() external {
+// CONCEPTUAL - getModifiedAccounts() is not a real cheatcode
+function assertionNoUnsafeDebt() external view {
     ph.forkPostTx();
-    
+
     // Get all accounts that were modified in this tx
+    // NOTE: This cheatcode does not exist - this is conceptual
     address[] memory accounts = ph.getModifiedAccounts();
-    
+
     for (uint256 i = 0; i < accounts.length; i++) {
         address account = accounts[i];
-        
+
         // Core invariant: Collateral must always be >= Debt
         require(euler.healthCheck(account), "Account has more debt than collateral");
     }
 }
 ```
 
-This assertion ensures that users don't have more debt than collateral after the transaction.
+The key insight is that the **invariant itself is simple**: after any transaction, no account should have more debt than collateral. The challenge is identifying which accounts to check, which in a real implementation might require parsing transaction logs or call inputs.
 
 ## Additional Considerations
 

assertions-book/previous-hacks/first-depositor.mdx

@@ -61,12 +61,11 @@ function assertionHasMinimumSupply() public view {
 function assertionExchangeRate() public view {
     Market market = Market(address(0x1234));
 
-
-    PhEvm.CallInputs[] memory inputs = PhEvm.CallInputs(address(cToken),abi.encodeWithSelector(cToken.mint.selector));
+    PhEvm.CallInputs[] memory inputs = ph.getCallInputs(address(cToken), cToken.mint.selector);
 
     for (uint256 i = 0; i < inputs.length; i++) {
         PhEvm.CallInputs memory input = inputs[i];
-        (address target, uint256 amount) = abi.decode(input.data, (address, uint256));
+        (uint256 amount) = abi.decode(input.input, (uint256));
         require(amount / market.exchangeRate() > 0, "Did not receive any shares");
     }
 }

assertions-book/previous-hacks/hack1-radiant-capital.mdx

@@ -40,42 +40,37 @@ contract LendingPoolAddressesProviderAssertions is Assertion {
         ILendingPoolAddressesProvider(0x091d52CacE1edc5527C99cDCFA6937C1635330E4); //arbitrum
 
     function triggers() external view override {
-        registerCallTrigger(this.assertionOwnerChange.selector, lendingPoolAddressesProvider.owner.selector);
-        registerCallTrigger(this.assertionEmergencyAdminChange.selector, lendingPoolAddressesProvider.getEmergencyAdmin.selector);
-        registerCallTrigger(this.assertionPoolAdminChange.selector, lendingPoolAddressesProvider.getPoolAdmin.selector);
+        // Trigger on any storage change to catch ownership modifications
+        registerStorageChangeTrigger(this.assertionOwnerChange.selector);
+        registerStorageChangeTrigger(this.assertionEmergencyAdminChange.selector);
+        registerStorageChangeTrigger(this.assertionPoolAdminChange.selector);
     }
 
     // Check if the owner has changed
-    // return true indicates a valid state -> owner is the same
-    // return false indicates an invalid state -> owner is different
-    function assertionOwnerChange() external returns (bool) {
+    function assertionOwnerChange() external view {
         ph.forkPreTx();
         address prevOwner = lendingPoolAddressesProvider.owner();
         ph.forkPostTx();
         address newOwner = lendingPoolAddressesProvider.owner();
-        return prevOwner == newOwner;
+        require(prevOwner == newOwner, "Owner has changed");
     }
 
     // Check if the emergency admin has changed
-    // return true indicates a valid state -> emergency admin is the same
-    // return false indicates an invalid state -> emergency admin is different
-    function assertionEmergencyAdminChange() external returns (bool) {
+    function assertionEmergencyAdminChange() external view {
         ph.forkPreTx();
         address prevEmergencyAdmin = lendingPoolAddressesProvider.getEmergencyAdmin();
         ph.forkPostTx();
         address newEmergencyAdmin = lendingPoolAddressesProvider.getEmergencyAdmin();
-        return prevEmergencyAdmin == newEmergencyAdmin;
+        require(prevEmergencyAdmin == newEmergencyAdmin, "Emergency admin has changed");
     }
 
     // Check if the pool admin has changed
-    // return true indicates a valid state -> pool admin is the same
-    // return false indicates an invalid state -> pool admin is different
-    function assertionPoolAdminChange() external returns (bool) {
+    function assertionPoolAdminChange() external view {
         ph.forkPreTx();
         address prevPoolAdmin = lendingPoolAddressesProvider.getPoolAdmin();
         ph.forkPostTx();
         address newPoolAdmin = lendingPoolAddressesProvider.getPoolAdmin();
-        return prevPoolAdmin == newPoolAdmin;
+        require(prevPoolAdmin == newPoolAdmin, "Pool admin has changed");
     }
 }
 ```

assertions-book/previous-hacks/hack2-vestra-dao.mdx

@@ -54,16 +54,19 @@ contract VestraDAOHack is Assertion {
         registerCallTrigger(this.assertionExample.selector, vestraDAO.unStake.selector);
     }
 
-    // Check if the user has already unstaked for a maturity
-    function assertionExample() external {
-        ph.forkPostTx();
+    // Check that user was actively staked before unstaking
+    // This prevents double-unstaking by ensuring isActive was true before the call
+    function assertionExample() external view {
         PhEvm.CallInputs[] memory unStakes = ph.getCallInputs(address(vestraDAO), vestraDAO.unStake.selector);
 
         for (uint256 i = 0; i < unStakes.length; i++) {
-            uint8 maturity = abi.decode(unStakes[i].input.maturity, (uint8));
+            uint8 maturity = abi.decode(unStakes[i].input, (uint8));
             address from = unStakes[i].caller;
-            IVestraDAO.Stake storage user = vestraDAO.stakes[from][maturity];
-            require(user.isActive, "User has already unstaked for this maturity");
+
+            // Check BEFORE the unstake that the stake was active
+            ph.forkPreCall(unStakes[i].id);
+            (,,,,,bool wasActive) = vestraDAO.stakes(from, maturity);
+            require(wasActive, "User was not actively staked for this maturity");
         }
     }
 }