IEEE-754 Float Inspector

Inspectable records

Ledger state

The current ledger marks this instrument verified clean within the source-bound verification corpus.

Area

Computing & Information

Tranche

tranche-2

Evidence ID

t2-016

Ledger rows

1

No ledger note is attached.

Review findings

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.

Formula and scope findings

• 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.

Unit assumptions

• 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.

Boundary hardening

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.

Errata and corrections

No applied erratum is attached to this unique-name record.

Inspectable example

4 review vectors are recorded. One source-bound sample is shown below.

{
  "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."
}

Related workflows

No source-defined multi-instrument workflow membership is recorded.

Sources and evidence

These pointers bind the page to evidence. They do not grant authority or collapse verification into deployment.

• VERIFIED_LEDGER.json · VERIFIED_CLEAN
• evidence-tranche2/tranche2-results.json
• BOUNDARY_HAZARD_CATALOG.json