Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Mathematical Specifications

Overview

Bitcoin Commons documents Orange Paper–aligned mathematical specifications for consensus behavior. The Rust code implements this spec, checked by tests and BLVM Specification Lock on spec-locked functions. Proof scope: PROOF_LIMITATIONS.md.

Specification Format

Mathematical specifications use formal notation to define consensus rules:

  • Quantifiers: Universal (∀) and existential (∃) quantifiers
  • Functions: Mathematical function definitions
  • Invariants: Properties that must always hold
  • Constraints: Bounds and limits

Code: VERIFICATION.md

Core Specifications

Chain Selection

Mathematical Specification:

∀ chains C₁, C₂: work(C₁) > work(C₂) ⇒ select(C₁)

Invariants:

  • Selected chain has maximum cumulative work
  • Work calculation is deterministic
  • Empty chains are rejected
  • Chain work is always non-negative

Key functions:

  • should_reorganize: Longest-work selection
  • calculate_chain_work: Cumulative work calculation
  • expand_target: Difficulty target edge cases (see also PoW specs)

Code: VERIFICATION.md

Block Subsidy

Mathematical Specification:

∀ h ∈ ℕ: subsidy(h) = 50 * 10^8 * 2^(-⌊h/210000⌋) if ⌊h/210000⌋ < 64 else 0

Invariants:

  • Subsidy halves every 210,000 blocks
  • Subsidy is non-negative
  • Subsidy decreases monotonically
  • Total supply converges to 21 million BTC

Code: VERIFICATION.md

Total Supply

Mathematical Specification:

∀ h ∈ ℕ: total_supply(h) = Σ(i=0 to h) subsidy(i)

Invariants:

  • Total supply is monotonic (never decreases)
  • Total supply is bounded (≤ 21 * 10^6 * 10^8 satoshis)
  • Total supply converges to 21 million BTC

Code: PROOF_LIMITATIONS.md

Difficulty Adjustment

Mathematical Specification:

target_new = target_old * (timespan / expected_timespan)
timespan_clamped = clamp(timespan, expected/4, expected*4)

Invariants:

  • Target is always positive
  • Timespan is clamped to [expected/4, expected*4]
  • Difficulty adjustment is deterministic

Code: VERIFICATION.md

Consensus Threshold

Mathematical Specification:

required_agreement_count = ceil(total_peers * threshold)
consensus_met ⟺ agreement_count >= required_agreement_count

Invariants:

  • 1 <= required_agreement_count <= total_peers
  • agreement_count >= required ⟺ ratio >= threshold
  • Integer comparison is deterministic

Code: VERIFICATION.md

Median Calculation

Mathematical Specification:

median(tips) = {
    tips[n/2] if n is odd,
    (tips[n/2-1] + tips[n/2]) / 2 if n is even
}

Invariants:

  • min(tips) <= median <= max(tips)
  • Median is deterministic
  • Checkpoint = max(0, median - safety_margin)

Code: VERIFICATION.md

Specification Coverage

Functions with Specifications

Multiple functions have formal mathematical specifications:

  • Chain selection (should_reorganize, calculate_chain_work)
  • Block subsidy (get_block_subsidy)
  • Total supply (total_supply)
  • Difficulty adjustment (get_next_work_required, expand_target)
  • Transaction validation (check_transaction, check_tx_inputs)
  • Block validation (connect_block, apply_transaction)
  • Script execution (eval_script, verify_script)
  • Consensus threshold (find_consensus)
  • Median calculation (determine_checkpoint_height)

Code: PROOF_LIMITATIONS.md

Mathematical Protections

Integer-Based Arithmetic

Floating-point arithmetic replaced with integer-based calculations:

#![allow(unused)]
fn main() {
// Integer-based threshold calculation
let required_agreement_count = ((total_peers as f64) * threshold).ceil() as usize;
if agreement_count >= required_agreement_count {
    // Consensus met
}
}

Code: VERIFICATION.md

Runtime Assertions

Runtime assertions verify mathematical invariants:

  • Threshold calculation bounds
  • Consensus result invariants
  • Median calculation bounds
  • Checkpoint bounds

Code: VERIFICATION.md

Checked Arithmetic

Checked arithmetic prevents overflow/underflow:

#![allow(unused)]
fn main() {
// Median calculation with overflow protection
let median_tip = if sorted_tips.len() % 2 == 0 {
    let mid = sorted_tips.len() / 2;
    let lower = sorted_tips[mid - 1];
    let upper = sorted_tips[mid];
    (lower + upper) / 2  // Safe: Natural type prevents overflow
} else {
    sorted_tips[sorted_tips.len() / 2]
};
}

Code: VERIFICATION.md

Formal Verification

Z3 Proofs

BLVM Specification Lock uses Z3 to prove spec-locked functions against Orange Paper contracts. The symbolic specs above are not each a separate Z3 theorem; see PROOF_LIMITATIONS.md.

Code: VERIFICATION.md

Property-Based Tests

Property-based tests verify invariants:

  • Generate random inputs
  • Verify properties hold
  • Discover edge cases
  • Test mathematical correctness

Code: VERIFICATION.md

Documentation

Specification Documents

Mathematical specifications and verification are documented in the consensus repository (see docs/README.md):

Code: README.md

Components

The mathematical specifications system includes:

  • Formal mathematical notation for consensus functions
  • Mathematical invariants documentation
  • Integer-based arithmetic (prevents floating-point bugs)
  • Runtime assertions (verify invariants)
  • Checked arithmetic (prevents overflow)
  • BLVM Specification Lock / Z3 where enabled on annotated functions
  • Property-based tests (invariant verification)

Location: blvm-consensus/docs/VERIFICATION.md, blvm-consensus/docs/PROOF_LIMITATIONS.md, blvm-consensus/docs/README.md (index)

See Also