// Certora Specification for BondManager
// Verifies economic security properties and state invariants

using BondManager as BM;

// Import required contracts
import "../contracts/bridge/trustless/BondManager.sol";

// ============================================================================
// INVARIANTS
// ============================================================================

// Invariant: Bond cannot be both slashed and released
invariant bondStateExclusive(uint256 depositId)
    BM.bonds(depositId).slashed == false || BM.bonds(depositId).released == false;

// Invariant: Total bonds tracking is consistent
invariant totalBondsConsistency(address relayer)
    BM.totalBonds(relayer) == sum(depositId => 
        BM.bonds(depositId).relayer == relayer && 
        !BM.bonds(depositId).slashed && 
        !BM.bonds(depositId).released ? 
        BM.bonds(depositId).amount : 0
    );

// ============================================================================
// RULES FOR postBond
// ============================================================================

// Rule: Bond calculation is correct
rule bondCalculationCorrect(uint256 depositId, uint256 depositAmount, address relayer) {
    env e;
    uint256 requiredBond = BM.getRequiredBond(depositAmount);
    uint256 calculatedBond = (depositAmount * BM.bondMultiplier()) / 10000;
    uint256 minBond = BM.minBond();
    
    // Bond must be at least the calculated amount or minimum
    assert requiredBond >= calculatedBond || requiredBond >= minBond;
    assert requiredBond == (calculatedBond > minBond ? calculatedBond : minBond);
    
    // If posting bond, amount must be >= required
    uint256 bondAmount = BM.postBond@withrevert(e, depositId, depositAmount, relayer);
    if (!lastReverted) {
        assert bondAmount >= requiredBond;
    }
}

// Rule: Bond cannot be posted twice for same depositId
rule noDuplicateBonds(uint256 depositId, uint256 depositAmount1, uint256 depositAmount2, address relayer) {
    env e1, e2;
    
    // First bond post succeeds
    BM.postBond(e1, depositId, depositAmount1, relayer);
    assume !lastReverted;
    
    // Second bond post must fail
    BM.postBond@withrevert(e2, depositId, depositAmount2, relayer);
    assert lastReverted;
}

// Rule: Total bonds updated correctly on post
rule totalBondsUpdatedOnPost(uint256 depositId, uint256 depositAmount, address relayer) {
    env e;
    uint256 totalBefore = BM.totalBonds(relayer);
    uint256 bondAmount = BM.postBond@withrevert(e, depositId, depositAmount, relayer);
    
    if (!lastReverted) {
        uint256 totalAfter = BM.totalBonds(relayer);
        assert totalAfter == totalBefore + bondAmount;
    }
}

// ============================================================================
// RULES FOR slashBond
// ============================================================================

// Rule: Bond cannot be slashed if already released
rule cannotSlashReleasedBond(uint256 depositId, address challenger) {
    env e1, e2;
    
    // Release bond first
    BM.releaseBond(e1, depositId);
    assume !lastReverted;
    
    // Slashing must fail
    BM.slashBond@withrevert(e2, depositId, challenger);
    assert lastReverted;
}

// Rule: Bond cannot be slashed if already slashed
rule cannotSlashTwice(uint256 depositId, address challenger1, address challenger2) {
    env e1, e2;
    
    // First slash succeeds
    BM.slashBond(e1, depositId, challenger1);
    assume !lastReverted;
    
    // Second slash must fail
    BM.slashBond@withrevert(e2, depositId, challenger2);
    assert lastReverted;
}

// Rule: Slashing splits 50/50 correctly
rule slashingSplitCorrect(uint256 depositId, address challenger) {
    env e;
    uint256 bondAmountBefore = BM.bonds(depositId).amount;
    
    (uint256 challengerReward, uint256 burnedAmount) = BM.slashBond@withrevert(e, depositId, challenger);
    
    if (!lastReverted) {
        // Challenger gets 50% (or slightly more for odd amounts)
        assert challengerReward == bondAmountBefore / 2 || challengerReward == bondAmountBefore / 2 + 1;
        // Burned amount is remainder
        assert challengerReward + burnedAmount == bondAmountBefore;
        // Bond marked as slashed
        assert BM.bonds(depositId).slashed == true;
    }
}

// Rule: Total bonds decreased on slash
rule totalBondsDecreasedOnSlash(uint256 depositId, address challenger) {
    env e;
    address relayer = BM.bonds(depositId).relayer;
    uint256 totalBefore = BM.totalBonds(relayer);
    uint256 bondAmount = BM.bonds(depositId).amount;
    
    BM.slashBond@withrevert(e, depositId, challenger);
    
    if (!lastReverted) {
        uint256 totalAfter = BM.totalBonds(relayer);
        assert totalAfter == totalBefore - bondAmount;
    }
}

// ============================================================================
// RULES FOR releaseBond
// ============================================================================

// Rule: Bond cannot be released if already slashed
rule cannotReleaseSlashedBond(uint256 depositId) {
    env e1, e2;
    
    // Slash bond first
    address challenger = address(0x1234);
    BM.slashBond(e1, depositId, challenger);
    assume !lastReverted;
    
    // Release must fail
    BM.releaseBond@withrevert(e2, depositId);
    assert lastReverted;
}

// Rule: Bond cannot be released twice
rule cannotReleaseTwice(uint256 depositId) {
    env e1, e2;
    
    // First release succeeds
    BM.releaseBond(e1, depositId);
    assume !lastReverted;
    
    // Second release must fail
    BM.releaseBond@withrevert(e2, depositId);
    assert lastReverted;
}

// Rule: Total bonds decreased on release
rule totalBondsDecreasedOnRelease(uint256 depositId) {
    env e;
    address relayer = BM.bonds(depositId).relayer;
    uint256 totalBefore = BM.totalBonds(relayer);
    uint256 bondAmount = BM.bonds(depositId).amount;
    
    BM.releaseBond@withrevert(e, depositId);
    
    if (!lastReverted) {
        uint256 totalAfter = BM.totalBonds(relayer);
        assert totalAfter == totalBefore - bondAmount;
        // Bond marked as released
        assert BM.bonds(depositId).released == true;
    }
}

// ============================================================================
// RULES FOR getRequiredBond
// ============================================================================

// Rule: Bond calculation formula is correct
rule requiredBondFormula(uint256 depositAmount) {
    uint256 requiredBond = BM.getRequiredBond(depositAmount);
    uint256 calculatedBond = (depositAmount * BM.bondMultiplier()) / 10000;
    uint256 minBond = BM.minBond();
    
    // Required bond is max of calculated and minimum
    assert requiredBond == (calculatedBond > minBond ? calculatedBond : minBond);
    assert requiredBond >= minBond;
}

// Rule: Bond multiplier constraint (>= 100%)
rule bondMultiplierConstraint() {
    assert BM.bondMultiplier() >= 10000;
}

// Rule: Minimum bond is positive
rule minBondPositive() {
    assert BM.minBond() > 0;
}

// ============================================================================
// REENTRANCY PROTECTION
// ============================================================================

// Rule: No reentrancy in postBond
rule noReentrancyPostBond(uint256 depositId, uint256 depositAmount, address relayer) {
    env e;
    // Certora will check that nonReentrant modifier prevents reentrancy
    BM.postBond(e, depositId, depositAmount, relayer);
}

// Rule: No reentrancy in slashBond
rule noReentrancySlashBond(uint256 depositId, address challenger) {
    env e;
    BM.slashBond(e, depositId, challenger);
}

// Rule: No reentrancy in releaseBond
rule noReentrancyReleaseBond(uint256 depositId) {
    env e;
    BM.releaseBond(e, depositId);
}