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

// Deliberately broken arithmetic examples for an isolated local regression test.
// Not a deployable token or a production library.
contract ArithmeticCases {
    function normal(uint256 balance, uint256 amount) external pure returns (uint256) {
        require(amount <= balance, "insufficient balance");
        return balance - amount;
    }

    function zeroBranch(uint256 balance, uint256 amount) external pure returns (uint256) {
        if (amount == 1) return uint120(0);
        require(amount <= balance, "insufficient balance");
        return balance - amount;
    }

    function maxBranch(uint256 balance, uint256 amount) external pure returns (uint256) {
        if (amount == 1) return ~uint120(0);
        require(amount <= balance, "insufficient balance");
        return balance - amount;
    }
}

contract BalanceInvariantTest {
    ArithmeticCases private cases = new ArithmeticCases();

    function testMatrix16InputPairs() public view {
        uint256[4] memory values = [uint256(0), 1, 2, 10];
        uint256 zeroDifferences;
        uint256 maxDifferences;
        for (uint256 i; i < values.length; i++) {
            for (uint256 j; j < values.length; j++) {
                (bool normalOk, bytes memory normalValue) = address(cases).staticcall(
                    abi.encodeCall(cases.normal, (values[i], values[j]))
                );
                (bool zeroOk, bytes memory zeroValue) = address(cases).staticcall(
                    abi.encodeCall(cases.zeroBranch, (values[i], values[j]))
                );
                (bool maxOk, bytes memory maxValue) = address(cases).staticcall(
                    abi.encodeCall(cases.maxBranch, (values[i], values[j]))
                );
                if (zeroOk != normalOk || (zeroOk && keccak256(zeroValue) != keccak256(normalValue))) zeroDifferences++;
                if (maxOk != normalOk || (maxOk && keccak256(maxValue) != keccak256(normalValue))) maxDifferences++;
            }
        }
        require(zeroDifferences == 3, "zero branch mismatch count");
        require(maxDifferences == 4, "max branch mismatch count");
    }

    function testOneCharacterChangesTheResult() public view {
        require(cases.zeroBranch(10, 1) == 0, "zero cast");
        require(cases.maxBranch(10, 1) == 1329227995784915872903807060280344575, "complement");
    }

    function testRecordedSupplyCanHideBalanceInflation() public view {
        uint256 recordedSupply = 10;
        uint256 senderAfter = cases.maxBranch(10, 1);
        uint256 recipientAfter = 1;
        require(senderAfter + recipientAfter > recordedSupply, "broken balance invariant");
        require(recordedSupply == 10, "supply field was not changed");
    }
}