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

import {Test} from "forge-std/Test.sol";
import {ObseroWatchBoard} from "../src/ObseroWatchBoard.sol";

contract BoardHandler is Test {
    ObseroWatchBoard public board;
    address[3] public actors = [address(0x1001), address(0x1002), address(0x1003)];
    address[3] public targets = [address(0x2001), address(0x2002), address(0x2003)];
    uint256 public ghostPresets;
    uint256 public ghostRetired;
    mapping(address => uint256) public ghostPerTarget;
    mapping(address => uint256) public ghostPerActor;

    constructor(ObseroWatchBoard b) { board = b; }

    function publish(uint256 a, uint256 t, uint8 ruleSeed, uint8 labelLen) external {
        address who = actors[a % 3];
        address target = targets[t % 3];
        bytes memory rules = abi.encodePacked("rules-", ruleSeed % 6);
        string memory label = string(new bytes(bound(labelLen, 0, 50)));
        vm.prank(who);
        try board.publish(target, label, rules) returns (uint256) {
            ghostPresets++;
            ghostPerTarget[target]++;
            ghostPerActor[who]++;
        } catch {}
    }

    function retire(uint256 a, uint256 id) external {
        uint256 n = board.presetCount();
        if (n == 0) return;
        id = bound(id, 1, n);
        vm.prank(actors[a % 3]);
        try board.retire(id) {
            ghostRetired++;
        } catch {}
    }

    function roll(uint8 n) external { vm.roll(block.number + 1 + (n % 20)); }
}

contract ObseroWatchBoardInvariantTest is Test {
    ObseroWatchBoard board;
    BoardHandler handler;

    function setUp() public {
        vm.roll(100);
        board = new ObseroWatchBoard();
        handler = new BoardHandler(board);
        targetContract(address(handler));
    }

    function invariant_countsMatchGhost() public view {
        assertEq(board.presetCount(), handler.ghostPresets());
        uint256 sumTargets;
        uint256 sumActors;
        for (uint256 i = 0; i < 3; i++) {
            assertEq(board.targetPresetCount(handler.targets(i)), handler.ghostPerTarget(handler.targets(i)));
            assertEq(board.publisherPresetCount(handler.actors(i)), handler.ghostPerActor(handler.actors(i)));
            sumTargets += board.targetPresetCount(handler.targets(i));
            sumActors += board.publisherPresetCount(handler.actors(i));
        }
        assertEq(sumTargets, board.presetCount());
        assertEq(sumActors, board.presetCount());
    }

    function invariant_presetsConsistent() public view {
        uint256 n = board.presetCount();
        uint64 lastBlock;
        uint256 retired;
        for (uint256 id = 1; id <= n; id++) {
            ObseroWatchBoard.Preset memory p = board.preset(id);
            assertTrue(p.target != address(0));
            assertTrue(bytes(p.label).length >= 1 && bytes(p.label).length <= board.MAX_LABEL());
            assertEq(board.presetOf(p.publisher, p.target, p.rulesHash), id);
            assertGe(p.publishedBlock, lastBlock);
            lastBlock = p.publishedBlock;
            if (p.retired) retired++;
        }
        assertEq(retired, handler.ghostRetired());
    }

    function invariant_holdsNoEth() public view {
        assertEq(address(board).balance, 0);
    }
}