Module proven_bounds 

Proven bounds for runtime optimization

These bounds are proven by formal verification and can be used for runtime optimizations without additional safety checks.

Proven runtime bounds for BLVM optimizations

These bounds have been formally proven and are used for runtime optimizations. Unlike proof-time limits (in _helpers::proof_limits), these represent actual Bitcoin limits that have been proven to hold in all cases.

Reference: BLVM Optimization Pass

Constants

MAX_BLOCK_SIZE_PROVEN

Maximum block size (proven by formal verification in block.rs)

MAX_INPUTS_PROVEN

Maximum inputs per transaction (proven by formal verification) References actual Bitcoin limit from constants.rs

MAX_OUTPUTS_PROVEN

Maximum outputs per transaction (proven by formal verification) References actual Bitcoin limit from constants.rs

MAX_PREV_HEADERS_PROVEN

Maximum previous headers for difficulty adjustment (proven by formal verification)

MAX_TRANSACTIONS_PROVEN

Maximum transactions per block (proven by formal verification) Note: Bitcoin limit is effectively unbounded by consensus rules, but practical limit is around 10,000 transactions per block based on block size limits.

MAX_TX_SIZE_PROVEN

Maximum transaction size (proven by formal verification in transaction.rs)