From 2e69968a8f5f73a2734e522e356a09ef04e14d28 Mon Sep 17 00:00:00 2001
From: Kevin Gibbons <bakkot@gmail.com>
Date: Wed, 4 Dec 2024 21:15:02 -0800
Subject: [PATCH] Editorial: add note about casting to f16 (#14)

---
 spec.html | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/spec.html b/spec.html
index 5993bd4..270f086 100644
--- a/spec.html
+++ b/spec.html
@@ -42,6 +42,11 @@ <h1><ins>Math.f16round ( _x_ )</ins></h1>
       1. Let _n64_ be the result of converting _n16_ to IEEE 754-2019 binary64 format.
       1. Return the ECMAScript Number value corresponding to _n64_.
     </emu-alg>
+
+    <emu-note>
+      <p>This operation is not the same as casting to binary32 and then to binary16 because of the possibility of double-rounding: consider the number _k_ = *1.00048828125000022204*<sub>𝔽</sub>, for example, for which which Math.f16round(_k_) is *1.0009765625*<sub>𝔽</sub>, but Math.f16round(Math.fround(_k_)) is *1*<sub>𝔽</sub>.</p>
+      <p>Not all platforms provide native support for casting from binary64 to binary16. There are various libraries which can provide this, including the MIT-licensed <a href="https://half.sourceforge.net/">half</a> library. Alternatively, it is possible to first cast from binary64 to binary32 under roundTiesToEven and then check whether the result could lead to incorrect double-rounding. The cases which could can be handled explicitly by adjusting the mantissa of the binary32 value so that it is the value which would be produced by performing the initial cast under roundTiesToOdd. Casting the adjusted value to binary16 under roundTiesToEven then produces the correct value.</p>
+    </emu-note>
   </emu-clause>
 </emu-clause>