Correctness of native-word posit packing

The capability law immediately identifies direct native packing with exact model construction.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Configured.NativeCode.toModel_pack {format : Format} {plan : StoragePlan format} [NativeCode format plan] (bits : ℕ) (hbits : bits < format.modulus) : (pack bits hbits).toModel = Model.ofNatBits bits

Direct native-word packing decodes to the supplied complete posit encoding.