Widening binary16 to binary32 and narrowing back is the identity

Identifier: F:fp16-fp32-roundtrip-identity
Proof route: smt-clausal
External status: proved
Axiom footprint: ieee754-2019-conversion-semantics-as-encoded-by-axeyum-fp-to_fp-lowering, rounding-mode-roundNearestTiesToEven-on-both-legs, smtlib2-floatingpoint-sort-equality-one-nan-value-signed-zeros-distinct, tseitin-cnf-encoding-preserves-satisfiability, drat-refutation-semantics-as-implemented-by-axeyum-cnf-check-drat, formats-binary16-and-binary32-only-this-fact-is-not-format-generic

Recorded description

Let RNE denote roundNearestTiesToEven. For every value x of IEEE-754 binary16, SMT-LIB `(_ FloatingPoint 5 11)`, converting x to binary32 and converting the result back to binary16 -- both conversions under RNE -- yields x again: `((_ to_fp 5 11) RNE ((_ to_fp 8 24) RNE x)) = x`, where `=` is SMT-LIB equality on the FloatingPoint sort (one NaN value, +0 and -0 distinct). This is the property that makes a binary16 tensor safe to stage through a binary32 accumulator and read back.

Formal statement

(assert (= ((_ to_fp 5 11) RNE ((_ to_fp 8 24) RNE x)) x))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

fp16-fp32-roundtrip-unsat-drat

Kind: unsat-certificate
Status: checked

Supports: The negation of formal.statement is unsatisfiable, so the round trip is the identity on every binary16 value.

Checker command

test "$(cargo run --release -q -p axeyum-bench --example smtcomp_cli -- --evidence artifacts/facts/smt2/neg-fp16-fp32-roundtrip-identity.smt2 | tail -1)" = unsat

Evidence notes

Ran 2026-08-14: `; evidence kind=unsat-drat certified=1 recheck=ok arena=ok ms=6409`, verdict `unsat`, 9.6s wall in a release build. `recheck=ok` is axeyum's own `check_drat` (RUP+RAT) re-checking the emitted refutation; `arena=ok` is `Evidence::check` against a fresh parse. Cross-checked independently: `z3 -smt2` reports `unsat` (0.1s) and `bitwuzla 0.9.1` reports `unsat` (0.1s).

fp16-fp32-roundtrip-exhaustive-apfloat

Kind: exhaustive-enumeration
Status: checked

Supports: All 65536 binary16 encodings round-tripped through binary32 by LLVM's APFloat: zero values changed.

Checker command

cargo run --release -q -p axeyum-fp --example kernel_equivalence -- roundtrip-fp32

Evidence notes

Ran 2026-08-14, under a second. examined=65536 failures=0, sharing no code with axeyum's lowering. The same run also settles bfloat16 -> binary32 -> bfloat16 (2^16, zero failures) and fp8 E5M2 -> binary32 -> fp8 E5M2 (2^8, zero failures); those are neighbouring propositions, not this one. NaN is handled as SMT-LIB requires -- all NaN encodings are one value, so a NaN that returns with a different payload still counts as returning the same value; APFloat bit equality alone would have reported a spurious failure here.

Provenance

{
  "date": "2026-08-14",
  "established_by": "fp-kernels lane; axeyum SMT front door (QF_FP -> fpa2bv -> CNF -> DRAT) plus an independent exhaustive LLVM-APFloat enumeration",
  "source": "authored here; the mixed-precision-training question stated as a proposition rather than tested by sampling.",
  "prior_art": [
    {
      "who": "IEEE 754-2019, clause 5.4.2 (conversion operations)",
      "what": "That conversion to a format with both greater precision and greater exponent range is exact, hence invertible.",
      "where": "IEEE Standard for Floating-Point Arithmetic",
      "year": 2019,
      "attribution": "standard textbook attribution; this lane did not consult the primary source, and records the citation as the received one. Nothing in the evidence above depends on it -- binary32 having strictly more of both is checked here by enumeration, not assumed."
    }
  ]
}