Storage codecs for configured binary formats

Every storage plan uses the same canonical Code conversion pair. The plan is reducible, so a closed executable format specializes to its ordinary unboxed carrier.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.BinaryInterchange.Configured.canonicalCodec (format : FloatFormat) (plan : StoragePlan format) : ExecFloat.ModelCodec plan (Model format) (Code plan)

The canonical lossless codec for one statically known storage plan.

Keeping the record construction in one place avoids duplicating conversion code and inverse proofs across the primitive carriers.

@[reducible, inline]

instance FloatLib.Floats.Formats.BinaryInterchange.Configured.codecForPlan (format : FloatFormat) (plan : StoragePlan format) : ExecFloat.ModelCodec plan (Model format) (Code plan)

The lossless codec selected by an arbitrary static storage plan.

The match comes before the codec record because Lean's native compiler must see the selected primitive carrier before compiling the record projections. Otherwise a dependent UInt8, UInt16, UInt32, or UInt64 result can be given the boxed calling convention. Every branch uses the same generic codec definition.