Packing equivalence for configured binary formats

These theorems prove that configured packing and decoding are mutual inverses for every selected carrier. Codec instances reuse this equivalence instead of duplicating one proof for each machine-word width.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Code.toModel_ofModel {format : FloatFormat} {plan : StoragePlan format} (value : Model format) : (ofModel value).toModel = value

Decoding a freshly packed proof-model value returns that exact model.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Code.ofModel_toModel {format : FloatFormat} {plan : StoragePlan format} (code : Code plan) : ofModel code.toModel = code

Repacking a decoded runtime code returns the original packed code.