pub fn expand_target(bits: u64) -> Result<U256, ConsensusError>Expand description
Expand target from compact representation
Expand compact target representation to full U256 target
Bitcoin uses a compact representation for difficulty targets. The format is: 0x1d00ffff where:
- 0x1d is the exponent (29)
- 0x00ffff is the mantissa (65535)
The actual target is: mantissa * 2^(8 * (exponent - 3))
§Mathematical Specification (compact target format)
Implements SetCompact() algorithm for nBits.
The inverse operation is compress_target() which implements GetCompact().
Round-trip Property (Formally Verified): ∀ bits ∈ [0x03000000, 0x1d00ffff]:
- Let expanded = expand_target(bits)
- Let compressed = compress_target(expanded)
- Let re_expanded = expand_target(compressed)
- Then: re_expanded ≤ expanded (compression truncates lower bits)
- And: re_expanded.0[2] = expanded.0[2] ∧ re_expanded.0[3] = expanded.0[3] (significant bits preserved exactly)
§Verified by formally verified
The round-trip property is formally verified by _target_expand_compress_round_trip()
which proves the mathematical specification holds for all valid target values.