Vestra DAO Hack

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

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

// VestraDAO interface
interface IVestraDAO {
    struct Stake {
        uint64 startTime;
        uint256 stakeAmount;
        uint256 yield;
        uint256 penalty;
        uint64 endTime;
        bool isActive;
    }

    mapping(address => mapping(uint8 => Stake)) public stakes;

    function unStake(uint8 maturity) external;
}

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

    IVestraDAO public vestraDAO = IVestraDAO(address(0xbeef));

    function triggers() external view override {
        registerFnCallTrigger(this.assertionExample.selector, vestraDAO.unStake.selector);
    }

    // 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, (uint8));
            address from = unStakes[i].caller;

            // Check BEFORE the unstake that the stake was active
            PhEvm.ForkId memory preCallFork = PhEvm.ForkId({forkType: 2, callIndex: unStakes[i].id});
            (,,,,,bool wasActive) = vestraDAO.stakes(from, maturity);
            require(wasActive, "User was not actively staked for this maturity");
        }
    }
}