Ether Drain

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.13;

import {Assertion} from "credible-std/Assertion.sol";
import {AssertionSpec} from "credible-std/SpecRecorder.sol";
import {PhEvm} from "credible-std/PhEvm.sol";

contract EtherDrainAssertion is Assertion {
    constructor() {
        registerAssertionSpec(AssertionSpec.Reshiram);
    }

    // Maximum percentage of ETH that can be drained in a single transaction (10% by default)
    uint256 public constant MAX_DRAIN_PERCENTAGE = 10;

    function triggers() external view override {
        // Register a trigger that activates when the ETH balance of the monitored contract changes
        registerTxEndTrigger(this.assertionEtherDrain.selector);
    }

    // Combined assertion for ETH drain with whitelist logic
    function assertionEtherDrain() external {
        // Get the assertion adopter address (this is the contract we're monitoring)
        address exampleContract = ph.getAssertionAdopter();

        // Capture the ETH balance before transaction execution
        PhEvm.ForkId memory preFork = _preTx();
        uint256 preBalance = address(exampleContract).balance;

        // Capture the ETH balance after transaction execution
        PhEvm.ForkId memory postFork = _postTx();
        uint256 postBalance = address(exampleContract).balance;

        // Only check for drainage (we don't care about ETH being added)
        if (preBalance > postBalance) {
            // Calculate the amount drained and the maximum allowed drain
            uint256 drainAmount = preBalance - postBalance;
            uint256 maxAllowedDrain = (preBalance * MAX_DRAIN_PERCENTAGE) / 100;

            // If drain amount is within allowed limit, allow the transaction
            if (drainAmount <= maxAllowedDrain) {
                return; // Small drain, no need to check whitelist
            }

            // For large drains, we would need to check whitelist
            // Since we can't easily access constructor parameters in the new interface,
            // we'll use a simplified approach that just checks the drain percentage
            // In a real implementation, this would be more sophisticated
            revert("Large ETH drain detected - exceeds allowed percentage");
        }
    }
}

interface IExampleContract {}