Correct Withdraw

// SPDX-License-Identifier: MIT
pragma solidity 0.8.28;

import {Assertion} from "../../lib/credible-std/src/Assertion.sol";
import {PhEvm} from "../../lib/credible-std/src/PhEvm.sol";

interface IYieldFarm {
    function withdraw(uint256 amount) external;
    function userInfo(address user) external view returns (uint256 depositAmount, uint256 rewards);
}

contract YieldFarmWithdrawAssertion is Assertion {
    IYieldFarm public farm = IYieldFarm(address(0xbeef));

    function fnSelectors() external pure override returns (bytes4[] memory assertions) {
        assertions = new bytes4[](1);
        assertions[0] = this.assertWithdraw.selector;
    }

    // Make sure the withdraw amount is less than or equal to the deposit amount
    // We don't want anyone to be able to withdraw more than they should be able to
    // We're assuming that that rewards are accounted for separately
    function assertWithdraw() external {
        PhEvm.CallInputs[] memory callInputs = ph.getCallInputs(address(farm), farm.withdraw.selector);
        if (callInputs.length == 0) {
            return;
        }

        for (uint256 i = 0; i < callInputs.length; i++) {
            bytes memory data = callInputs[i].input;
            address user = callInputs[i].caller;
            uint256 withdrawAmount = abi.decode(stripSelector(data), (uint256));

            // Get pre-withdrawal state
            (uint256 preDeposit,) = farm.userInfo(user);

            require(withdrawAmount <= preDeposit, "Withdraw exceeds deposit");

            // Check post-withdrawal state
            ph.forkPostState();
            (uint256 postDeposit,) = farm.userInfo(user);

            // Verify deposit amount decreased correctly
            require(postDeposit == preDeposit - withdrawAmount, "Incorrect withdrawal amount");
        }
    }

    function stripSelector(bytes memory input) internal pure returns (bytes memory) {
        bytes memory paramData = new bytes(32);
        for (uint256 i = 4; i < input.length; i++) {
            paramData[i - 4] = input[i];
        }
        return paramData;
    }
}