BTCDecoded

/// Kani proof: Supply Convergence (Orange Paper Theorem 8.2)
///
/// Mathematical specification:
/// lim(h→∞) TotalSupply(h) = 21 × 10⁶ × C
///
/// This proves that the total supply converges to exactly 21 million BTC.
/// After 64 halvings (height 13,440,000), the subsidy becomes 0, so:
/// TotalSupply(13,440,000) = 50 × C × Σ(i=0 to 63) (1/2)^i = 100 × C × (1 - 2^-64)
/// For practical purposes, 2^-64 ≈ 0, so supply ≈ 21M BTC.
#[kani::proof]
fn kani_supply_convergence() {
    // Test convergence property: as height increases, supply approaches 21M
    // After 64 halvings (height = 13,440,000), subsidy = 0

    // Calculate supply at different heights to show convergence
    let height_after_64_halvings = HALVING_INTERVAL * 64;

    // Bound for tractability (test up to 10 halvings)
    let max_test_height = HALVING_INTERVAL * 10;
    kani::assume(max_test_height <= height_after_64_halvings);

    // Supply at height h approaches 21M as h increases
    // Formula: TotalSupply(h) = 50 × C × Σ(i=0 to min(63, ⌊h/H⌋)) (1/2)^i
    // Where H = HALVING_INTERVAL = 210,000

    // Test monotonic convergence: supply increases but never exceeds 21M
    let supply_at_max = total_supply(max_test_height);

    // Critical invariant: supply never exceeds maximum money (21M BTC)
    assert!(
        supply_at_max <= MAX_MONEY,
        "Supply Convergence: total supply must never exceed 21M BTC"
    );

    // Convergence property: after many halvings, supply approaches 21M
    // For height = HALVING_INTERVAL * 64, subsidy = 0, so supply is constant
    // The supply at this point is: 50 × C × (1 - (1/2)^64) / (1 - 1/2) = 100 × C × (1 - 2^-64)
    // Since 2^-64 is negligible, this is effectively 100 × C = 21M BTC

    // Verify supply is bounded and converges
    assert!(
        supply_at_max >= 0,
        "Supply Convergence: total supply must be non-negative"
    );

    // Supply increases monotonically until halvings stop
    if max_test_height > 0 {
        let supply_at_h_minus_1 = total_supply(max_test_height - 1);
        assert!(
            supply_at_max >= supply_at_h_minus_1,
            "Supply Convergence: supply must increase monotonically"
        );
    }
}