Page actions
instrument mechanism / verified-clean
IEEE-754 Float Inspector mechanism
The inspectable method record for IEEE-754 Float Inspector, kept separate from implementation and qualification.
Model scope
The current honest label is appropriate but incomplete. The instrument should explicitly state that the displayed reconstruction formula applies only to normalized finite values, define all IEEE-754 special cases, specify decimal conversion and rounding behavior, and provide an exact ULP-error definition. The final test vector demonstrates a unit/spacing trap: for 0.1f the local float32 spacing is 2^-27, so the ULP error is 0.2, not 0.1.
- The reconstruction formula is valid only for normalized finite values. It is incorrect for zero, subnormal numbers, infinities, and NaNs.
- For normalized values, exp must mean the stored exponent field E and the exponent must be E minus the format bias; this is not stated precisely.
- Subnormal reconstruction is missing: value=(-1)^s·(0.mantissa)·2^(1-bias), with no implicit leading 1.
- Zero and signed zero special cases are missing; both exponent and mantissa fields are zero, but the reconstructed value is ±0 rather than 1·2^(-bias).
- Infinity and NaN encodings, where the exponent field is all ones, are not defined.
- No formula defines ULP error, and the result depends on whether the reference is the exact decimal input, a binary value, or another float. ULP spacing also differs at subnormal values and zero.
Units and conventions
- Bit fields, exponents, mantissas, and ULP counts are dimensionless; hexadecimal values represent raw bit patterns, not numeric magnitudes.
- The radix is 2.
- For normalized float32 values, bias=127, fraction width=23, and the spacing at unbiased exponent e is 2^(e-23).
- For normalized float64 values, bias=1023, fraction width=52, and the spacing at unbiased exponent e is 2^(e-52).
- For decimal-input vectors, the decimal is treated as an exact real number before round-to-nearest, ties-to-even conversion to the selected IEEE-754 format.
- The test-vector ULP error is defined as (reconstructed_value-exact_decimal_input)/local_spacing; this definition is not present in the supplied specification.
Inspectable vector
One of 4 source-bound review vectors:
{
"inputs": {
"decimal": 1.5,
"precision": 64
},
"expected_outputs": {
"sign_bits": "0",
"exponent_bits": "01111111111",
"mantissa_bits": "1000000000000000000000000000000000000000000000000000",
"raw_hex": "0x3FF8000000000000",
"decimal_reconstruction": 1.5,
"ulp_error": 0
},
"working": "1.5 = 1 + 1/2 = 1.1₂. The unbiased exponent is 0, so E=0+1023=1023=01111111111₂. Sign s=0. The fraction field is 1000...000₂, or 0x8000000000000. Reconstruct: (+1)·(1+1/2)·2^0 = 1.5. The decimal input is exactly representable, so rounding error=1.5-1.5=0 and ULP error=0."
}Failure boundary
BREAK_CLAIMED · SELF_FLAGGED
The stated normal-number formula is invalid for zero, subnormals, infinities, and NaNs, and raw hexadecimal input is ambiguous without an explicit word-versus-byte-order convention.
Other records
Sources and evidence
These pointers bind the page to evidence. They do not grant authority or collapse verification into deployment.
VERIFIED_LEDGER.jsonevidence-tranche2/tranche2-results.jsonBOUNDARY_HAZARD_CATALOG.json