This will help with proving correctness of Pack. Also, while doing so, create a UnpackedFloat.IsPackable predicate which enables us to show that a particular unpacked float can be packed Similarly, one for EUnpackedFloat.IsPackable. The main ones that are packable are (a) results of PackedFloat.unpack and (b) results of UnpackedFloat.round.
This will help with proving correctness of Pack. Also, while doing so, create a
UnpackedFloat.IsPackablepredicate which enables us to show that a particular unpacked float can be packed Similarly, one forEUnpackedFloat.IsPackable. The main ones that are packable are (a) results ofPackedFloat.unpackand (b) results ofUnpackedFloat.round.