Configured posit ExecFloat values

Import this module to use posits. The standard widths are Posit8, Posit16, Posit32, and Posit64, and any other width is selected by its total encoded width:

def x : Posit32 := 1.5
def y : ExecFloat.Posit (bits := 12) := 0.75

Every configured posit is an ordinary ExecFloat value, uses a statically selected carrier, and exposes its exact semantics through the common proof infrastructure.

Configured.Type owns the public type constructor, the modules below Configured.Storage own packed-carrier selection and codecs, and Configured.Plan.Dispatch installs certified operation backends. The value layer is split further:

• Configured.Value.Runtime provides packing, decoding, classification, and raw-word conversion;
• Configured.Instances installs comparison, display, literals, and negation;
• Configured.Value.Proof proves round trips, special-value semantics, and comparison laws.

Raw words are deliberately lower-level than ordinary numeric construction. They are for serialization, conformance vectors, and encoding proofs. Arithmetic clients should use numeric literals and the operation interface once the matching certified capability is imported.

References

• Posit Working Group, Standard for Posit Arithmetic (2022), March 2, 2022, https://posithub.org/docs/posit_standard-2.pdf.
• John L. Gustafson, Standard Posit Arithmetic, Supercomputing Frontiers and Innovations 9(1), 2022, https://doi.org/10.14529/jsfi220102.