Runtime packing for configured binary formats

Code.toModel and Code.ofModel are the single executable conversion pair for every built-in carrier. Range proofs are erased. The word16, word32, word64, and pair plans use the carrier's stored range proof to avoid computing powers of two or remainders during decoding. Code.Proof shows that packing and decoding are mutual inverses for every plan.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Code.toModel {format : FloatFormat} {plan : StoragePlan format} : Code plan → Model format

Interpret a packed runtime code in the exact-width proof model.

The machine-word and two-word carriers already carry the proof that their natural-number view is below 2 ^ format.bitWidth, so the model word is built with BitVec.ofNatLT and compiled code performs no modular reduction and no power computation on the decode path. For a single machine word the conversion is the unboxing of the word. The byte carrier keeps the canonical Model.ofNatBits decoder because the byte tier executes exhaustive tables, whose proofs are stated in terms of that decoder.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Code.ofModel {format : FloatFormat} {plan : StoragePlan format} : Model format → Code plan

Pack a proof-model value into the statically selected runtime code.