Storage codecs for configured binary formats

Every storage plan uses the same canonical Code conversion pair. The plan remains reducible, so a closed executable format still 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 deliberately precedes codec-record construction. 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 assigned the boxed calling convention. All branches still use the same generic codec definition.