Foundry Invariant Tests: How to Catch the Batch Bypass

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

import {Test} from "forge-std/Test.sol";
import {uRWA1155} from "../contracts/uRWA1155.sol";

contract BatchHandler is Test {
    uRWA1155 public immutable token;
    address public immutable holder;
    address public immutable dest;
    bool public viewSaidNoButExecuted; // ghost variable

    constructor(uRWA1155 token_, address holder_, address dest_) {
        token = token_;
        holder = holder_;
        dest = dest_;
    }

    function batch(uint256 len, bool toSelf, uint256[4] calldata seedIds, uint256[4] calldata seedValues) external {
        address to = toSelf ? holder : dest;
        uint256 n = bound(len, 1, 4);
        uint256[] memory ids = new uint256[](n);
        uint256[] memory values = new uint256[](n);
        uint256[3] memory total;
        for (uint256 i; i < n; ++i) {
            ids[i] = 1 + (seedIds[i] % 2);
            values[i] = bound(seedValues[i], 0, 100);
            total[ids[i]] += values[i];
        }

        vm.startPrank(holder);
        bool allowed1 = token.canTransfer(holder, to, 1, total[1]);
        bool allowed2 = token.canTransfer(holder, to, 2, total[2]);
        try token.safeBatchTransferFrom(holder, to, ids, values, "") {
            if (!allowed1 || !allowed2) viewSaidNoButExecuted = true;
        } catch {}
        vm.stopPrank();
    }
}

contract FrozenBalanceInvariantTest is Test {
    uRWA1155 internal token;
    BatchHandler internal handler;
    address internal admin = makeAddr("admin");
    address internal holder = makeAddr("holder");
    address internal dest = makeAddr("dest");

    function setUp() public {
        token = new uRWA1155("ipfs://meta/{id}.json", admin);
        vm.startPrank(admin);
        token.changeSendWhitelist(holder, true);
        token.changeReceiveWhitelist(holder, true);
        token.changeReceiveWhitelist(dest, true);
        for (uint256 id = 1; id <= 2; ++id) {
            token.mint(holder, id, 100);
            token.setFrozenTokens(holder, id, 60);
        }
        vm.stopPrank();

        handler = new BatchHandler(token, holder, dest);
        targetContract(address(handler));
    }

    function invariant_viewMatchesExecution() public view {
        assertFalse(handler.viewSaidNoButExecuted(), "batch executed what canTransfer refused");
    }

    function invariant_frozenTokensStayPut() public view {
        for (uint256 id = 1; id <= 2; ++id) {
            assertGe(token.balanceOf(holder, id), token.getFrozenTokens(holder, id), "frozen tokens left");
        }
    }

    function test_duplicateIdsCannotSpendFrozenTokens() public {
        uint256[] memory ids = new uint256[](2);
        uint256[] memory values = new uint256[](2);
        ids[0] = 1;
        ids[1] = 1;
        values[0] = 40;
        values[1] = 40;

        assertFalse(token.canTransfer(holder, dest, 1, 80));
        vm.prank(holder);
        vm.expectRevert();
        token.safeBatchTransferFrom(holder, dest, ids, values, "");
    }
}