Widening a packed binary word

Increasing the fraction width while retaining the exponent width shifts all three fields by the same number of bits. A single shift of the stored word therefore agrees with extracting and repacking its fields. The destination bound is proved before compilation, avoiding a modulus.

This is a storage identity for every bit pattern. The cast runtime separately checks bias and encoding compatibility and handles exceptional values before using it as a numerical conversion.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toNatBits_shiftLeft_lt {src dst : FloatFormat} (x : Model src) (he : src.expWidth = dst.expWidth) (hf : src.fracWidth ≤ dst.fracWidth) : x.toNatBits <<< (dst.fracWidth - src.fracWidth) < 2 ^ dst.bitWidth

Shifting a stored word by the added fraction width fits the destination storage.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.widenBits {src dst : FloatFormat} (x : Model src) (he : src.expWidth = dst.expWidth) (hf : src.fracWidth ≤ dst.fracWidth) : Model dst

Increase the stored fraction width by shifting the entire word.

This operation preserves fields, without interpreting them. Numerical casts must additionally check bias and encoding compatibility and apply their exceptional-value policy.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.widenBits_eq_ofFields {src dst : FloatFormat} (x : Model src) (he : src.expWidth = dst.expWidth) (hf : src.fracWidth ≤ dst.fracWidth) : x.widenBits he hf = ofFields dst x.signBit x.expField (x.fracField <<< (dst.fracWidth - src.fracWidth))

Shifting the complete word agrees bit for bit with widening its explicit fields.