Testing Infrastructure

Overview

Bitcoin Commons uses a multi-layered testing strategy combining formal verification, property-based testing, fuzzing, integration tests, and runtime assertions. This approach ensures correctness across consensus-critical code.

Testing Strategy

Layered Verification

The testing strategy uses multiple complementary techniques:

1. Formal Verification: Proves correctness for all inputs (bounded)
2. Property-Based Testing (Proptest): Verifies invariants with random inputs (unbounded)
3. Fuzzing (libFuzzer): Discovers edge cases through random generation
4. Integration Tests: Verifies end-to-end correctness
5. Unit Tests: Tests individual functions
6. Runtime Assertions: Catches violations during execution
7. MIRI Integration: Detects undefined behavior

Code: CONSENSUS_COVERAGE_ASSESSMENT.md

Test Types

Unit Tests

Unit tests verify individual functions in isolation:

• Location: tests/ directory, #[test] functions
• Coverage: Public functions
• Examples: Transaction validation, block validation, script execution

Code: estimate_test_coverage.py

Property-Based Tests

Property-based tests verify mathematical invariants:

• Location: tests/consensus_property_tests.rs and other property test files
• Coverage: Mathematical invariants
• Tool: Proptest

Code: consensus_property_tests.rs

Integration Tests

Integration tests verify end-to-end correctness:

• Location: tests/integration/ directory
• Coverage: Multi-component scenarios
• Examples: BIP compliance, historical replay, mempool mining

Code: mod.rs

Fuzz Tests

Fuzz tests discover edge cases through random generation:

• Location: fuzz/fuzz_targets/ directory
• Tool: libFuzzer
• Coverage: Critical consensus functions

Code: README.md

Formal Verification

Formal verification verifies correctness for all inputs:

• Location: src/ and tests/ directories
• Formal Verification: Proofs with tiered execution system
• Coverage: Critical consensus functions
• Tool: Formal verification tooling

Code: formal-verification.md

Spec-Lock Formal Verification

blvm-spec-lock provides formal verification of consensus and UTXO operations:

• Coverage: Functions with #[spec_locked("section")] annotations
• Tool: blvm-spec-lock (Z3-based)
• Mathematical Specifications: Verifies compliance with Orange Paper sections

Verified Properties (via spec-lock):

• Consensus rules (transaction, block, script validation)
• UTXO set operations where annotated
• Cryptographic primitives

Code: blvm-spec-lock

See Also: UTXO Commitments - Verification workflow

Runtime Assertions

Runtime assertions catch violations during execution:

• Coverage: Critical paths with runtime assertions
• Production: Available via feature flag

Code: CONSENSUS_COVERAGE_ASSESSMENT.md

MIRI Integration

MIRI detects undefined behavior:

• CI Integration: Automated undefined behavior detection
• Coverage: Property tests and critical unit tests
• Tool: MIRI interpreter

Code: CONSENSUS_COVERAGE_ASSESSMENT.md

Coverage Statistics

Overall Coverage

Code: CONSENSUS_COVERAGE_ASSESSMENT.md

Coverage by Consensus Area

Verification coverage includes all major consensus areas:

• Economic Rules: Formal proofs, property tests, runtime assertions, and fuzz targets
• Proof of Work: Formal proofs, property tests, runtime assertions, and fuzz targets
• Transaction Validation: Formal proofs, property tests, runtime assertions, and fuzz targets
• Block Validation: Formal proofs, property tests, runtime assertions, and fuzz targets
• Script Execution: Formal proofs, property tests, runtime assertions, and fuzz targets
• Chain Reorganization: Formal proofs, property tests, and runtime assertions
• Cryptographic: Formal proofs, property tests, and runtime assertions
• Mempool: Formal proofs, runtime assertions, and fuzz targets
• SegWit: Formal proofs, runtime assertions, and fuzz targets
• Serialization: Formal proofs, runtime assertions, and fuzz targets

Code: EXACT_VERIFICATION_COUNTS.md

Running Tests

Run All Tests

cd blvm-consensus
cargo test

Run Specific Test Type

# Unit tests
cargo test --lib

# Property tests
cargo test --test consensus_property_tests

# Integration tests
cargo test --test integration

# Fuzz tests
cargo +nightly fuzz run transaction_validation

Run with MIRI

cargo +nightly miri test

Run blvm-spec-lock Proofs

cargo blvm-spec-lock

Code: formal-verification.md

Run Spec-Lock Verification

# Run spec-lock verification (requires cargo-spec-lock)
cargo spec-lock verify --crate-path .

Coverage Goals

Target Coverage

• blvm-spec-lock Proofs: All critical consensus functions
• Property Tests: All mathematical invariants
• Fuzz Targets: All critical validation paths
• Runtime Assertions: All critical code paths
• Integration Tests: All major workflows

Current Status

All coverage goals met:

• ✅ Formal proofs covering all critical functions
• ✅ Property test functions covering all invariants
• ✅ Fuzz targets covering all critical paths
• ✅ Runtime assertions in all critical paths
• ✅ Comprehensive integration test suite

Code: CONSENSUS_COVERAGE_ASSESSMENT.md

Test Organization

Directory Structure

blvm-consensus/
├── src/                    # Source code with blvm-spec-lock proofs
├── tests/
│   ├── consensus_property_tests.rs  # Main property tests
│   ├── integration/         # Integration tests
│   ├── unit/               # Unit tests
│   ├── fuzzing/            # Fuzzing helpers
│   └── verification/       # Verification tests
└── fuzz/
    └── fuzz_targets/        # Fuzz targets

Code:

Edge Case Coverage

Beyond Proof Bounds

Edge cases beyond blvm-spec-lock proof bounds are covered by:

1. Property-Based Testing: Random inputs of various sizes
2. Mainnet Block Tests: Real Bitcoin mainnet blocks
3. Integration Tests: Realistic scenarios
4. Fuzz Testing: Random generation

Code: PROOF_LIMITATIONS.md

Differential Testing

Bitcoin Core Comparison

Differential tests compare behavior with Bitcoin Core:

• Location: tests/integration/differential_tests.rs
• Purpose: Verify consistency with Bitcoin Core
• Coverage: Critical consensus functions

Code: differential_tests.rs

CI Integration

Automated Testing

All tests run in CI:

• Unit Tests: Required for merge
• Property Tests: Required for merge
• Integration Tests: Required for merge
• Fuzz Tests: Run on schedule
• blvm-spec-lock Proofs: Run separately, not blocking
• MIRI: Run on property tests and critical unit tests

Code: formal-verification.md

Test Metrics

• Property Test Functions: Multiple functions across all files
• Runtime Assertions: Multiple assertions (assert! and debug_assert!)
• Fuzz Targets: Multiple fuzz targets

Code: EXACT_VERIFICATION_COUNTS.md

Components

The testing infrastructure includes:

• Unit tests for all public functions
• Property-based tests for mathematical invariants
• Integration tests for end-to-end scenarios
• Fuzz tests for edge case discovery
• blvm-spec-lock proofs for formal verification
• Runtime assertions for execution-time checks
• MIRI integration for undefined behavior detection
• Differential tests for Bitcoin Core comparison

Location: blvm-consensus/tests/, blvm-consensus/fuzz/, blvm-consensus/src/

See Also

• Property-Based Testing - Verify mathematical invariants
• Fuzzing Infrastructure - Automated bug discovery
• Differential Testing - Compare with Bitcoin Core
• Benchmarking - Performance measurement
• Snapshot Testing - Output consistency verification
• Formal Verification - blvm-spec-lock model checking
• UTXO Commitments - Spec-lock verification for UTXO operations
• Contributing - Testing requirements for contributions