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

import {Test} from "forge-std/Test.sol";
import {DeepYieldVault} from "../../src/DeepYieldVault.sol";
import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
import {ERC20} from "@openzeppelin/contracts/token/ERC20/ERC20.sol";

contract MockUSDT is ERC20 {
    constructor() ERC20("USDT", "USDT") {}
    function mint(address to, uint256 amount) external { _mint(to, amount); }
    function decimals() public pure override returns (uint8) { return 18; }
}

/// Halmos symbolic tests for DeepYieldVault ERC-4626 invariants.
/// Halmos explores symbolic input space rather than concrete values,
/// proving invariants for ALL possible inputs (within bit constraints).
contract HalmosERC4626Test is Test {
    DeepYieldVault vault;
    MockUSDT asset;
    address admin = address(0xA);
    address guardian = address(0xB);
    address treasury = address(0xC);

    function setUp() public {
        asset = new MockUSDT();
        vault = new DeepYieldVault(
            IERC20(address(asset)),
            "dyTest",
            "dyT",
            admin,
            guardian,
            treasury,
            0  // no deposit cap
        );
    }

    /// Halmos: deposit-redeem round-trip never gives back MORE than deposited.
    /// (Bounds: small amounts to keep symbolic state space tractable.)
    function check_DepositRedeem_NoFreeMoney(uint96 amount) public {
        vm.assume(amount > 0 && amount < type(uint64).max);
        address user = address(0xDEAD);

        asset.mint(user, amount);
        vm.startPrank(user);
        asset.approve(address(vault), amount);
        uint256 shares = vault.deposit(amount, user);
        uint256 redeemed = vault.redeem(shares, user, user);
        vm.stopPrank();

        // Invariant: redeem cannot exceed deposit by more than rounding (<= 1 wei tolerance)
        assert(redeemed <= amount);
    }

    /// Halmos: totalAssets() >= 0 always (cannot underflow)
    function check_TotalAssets_NonNegative() public view {
        uint256 ta = vault.totalAssets();
        assert(ta >= 0);
    }

    /// Halmos: virtual shares offset prevents first-deposit attack
    function check_VirtualOffset_FirstDepositSafe(uint96 attackerAmt, uint96 victimAmt) public {
        vm.assume(attackerAmt > 0 && attackerAmt < 1e18);
        vm.assume(victimAmt > 0 && victimAmt < 1e18);

        address attacker = address(0xA77);
        address victim = address(0xBEEF);

        // Attacker deposits tiny then donates to inflate
        asset.mint(attacker, attackerAmt + 1e6);
        vm.startPrank(attacker);
        asset.approve(address(vault), attackerAmt);
        vault.deposit(attackerAmt, attacker);
        asset.transfer(address(vault), 1e6);  // donation
        vm.stopPrank();

        // Victim deposits
        asset.mint(victim, victimAmt);
        vm.startPrank(victim);
        asset.approve(address(vault), victimAmt);
        uint256 victimShares = vault.deposit(victimAmt, victim);
        vm.stopPrank();

        // Victim must receive non-zero shares (offset=3 prevents zero-share grief)
        assert(victimShares > 0);
    }
}