Configured posit ExecFloat values

Import this module to define a standard posit by its total encoded width:

abbrev P32 := ExecFloat.Posit (bits := 32)

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-facing implementation is separated 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 useful for serialization, conformance vectors, and encoding proofs; arithmetic clients should use numeric literals and the operation interface once the corresponding 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.