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

import {BankTestBase} from "./helpers/BankTestBase.sol";
import {BankV2} from "../src/BankV2.sol";
import {Options, Upgrades} from "openzeppelin-foundry-upgrades/Upgrades.sol";
import {BankV2Handler} from "./helpers/BankV2Handler.sol";

contract BankInvariantTest is BankTestBase {
    BankV2Handler internal handler;

    function setUp() public override {
        super.setUp();
        Options memory opts;
        opts.referenceContract = "BankV1.sol:BankV1";
        Upgrades.upgradeProxy(proxy, "BankV2.sol:BankV2", "", opts, owner);
        BankV2 bankV2 = BankV2(proxy);

        handler = new BankV2Handler(token, bankV2);
        vm.prank(owner);
        token.transferOwnership(address(handler));

        targetContract(address(handler));
        bytes4[] memory selectors = new bytes4[](4);
        selectors[0] = handler.deposit.selector;
        selectors[1] = handler.withdraw.selector;
        selectors[2] = handler.donate.selector;
        selectors[3] = handler.transfer.selector;
        targetSelector(FuzzSelector({addr: address(handler), selectors: selectors}));
    }

    function testHandlerExecutesDeterministicTrackedTransfer() public {
        handler.deposit(0, 40e6);

        handler.transfer(0, 0, 15e6);

        assertEq(bank.balanceOf(handler.actorAt(0)), 25e6);
        assertEq(bank.balanceOf(handler.actorAt(1)), 15e6);
        assertEq(handler.ghostTransferred(), 15e6);
        assertEq(bank.totalLiabilities(), 40e6);
        assertEq(token.balanceOf(address(bank)), 40e6);
    }

    function invariant_liabilitiesEqualTrackedBalances() public view {
        uint256 sum;
        for (uint256 i; i < handler.actorCount(); ++i) {
            sum += bank.balanceOf(handler.actorAt(i));
        }
        assertEq(sum, bank.totalLiabilities());
    }

    function invariant_reservesCoverLiabilities() public view {
        assertGe(token.balanceOf(address(bank)), bank.totalLiabilities());
    }

    function invariant_ghostAccountingMatchesChain() public view {
        assertEq(handler.ghostDeposited() - handler.ghostWithdrawn(), bank.totalLiabilities());
        assertEq(
            handler.ghostDeposited() + handler.ghostDonated() - handler.ghostWithdrawn(), token.balanceOf(address(bank))
        );
    }
}