Exact-width decimal sign and payload extraction

Packing a sign with a payload below f.signBase recovers both fields exactly. Payload extraction stays below that bound for every word of the format's bit width.

theorem FloatLib.Floats.Formats.DecimalInterchange.Bits.mul_add_lt_mul {high highBound low radix : ℕ} (hh : high < highBound) (hl : low < radix) : high * radix + low < highBound * radix

Packing two bounded fields stays below the product of their exclusive bounds.

theorem FloatLib.Floats.Formats.DecimalInterchange.Bits.pack_toNat (f : Format) (s : Bool) (n : ℕ) (h : n < f.signBase) : (pack f s n).toNat = (if s = true then f.signBase else 0) + n

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Bits.negative_pack (f : Format) (s : Bool) (n : ℕ) (h : n < f.signBase) : negative f (pack f s n) = s

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Bits.payload_pack (f : Format) (s : Bool) (n : ℕ) (h : n < f.signBase) : payload f (pack f s n) = n

theorem FloatLib.Floats.Formats.DecimalInterchange.Bits.payload_lt (f : Format) (word : BitVec f.bitWidth) : payload f word < f.signBase