Inspection for exact fixed-point codes #
The unbounded fixed-point core has exact integer-coefficient arithmetic and no overflow policy. Its inspection profile therefore emphasizes rational denotation, common-scale addition and subtraction, and heterogeneous multiplication with a composed scale.
This optional meta module registers #float_info without adding elaborator dependencies to the
runtime family. It also states the missing operations plainly so exactness is not mistaken for a
complete floating-point API.
Build the proof-aware description shared by the exact code and its configured ExecFloat
wrapper. The wrapper replaces carrier-specific execution and theorem entries while retaining this
single account of the value set, scale, and exact arithmetic.