[<prev] [next>] [<thread-prev] [day] [month] [year] [list]
Message-ID: <20260903133243.GP3542221@port70.net>
Date: Thu, 3 Sep 2026 15:32:43 +0200
From: Szabolcs Nagy <nsz@...t70.net>
To: Sergey Davidoff <shnatsel@...il.com>
Cc: Rich Felker <dalias@...c.org>, musl@...ts.openwall.com
Subject: Re: [PATCH v4 2/2] math: fmaf rewrite
* Sergey Davidoff <shnatsel@...il.com> [2026-09-03 09:32:19 +0100]:
> The algorithm from the v5 patch in
> https://www.openwall.com/lists/musl/2026/08/20/1 has been verified on
> an SMT solver and proven correct.
note the code is not correct under some fast-math flags.
> Here's the translation into an SMT-amenable language that was actually verified:
>
> https://dzaima.github.io/paste/#0hVLLbsIwELzzFVNVquI2SLwKKiW599x7kQU2WA0OcmyahIZv724CHKqiWors3Znszo69VhpeOXtcxfAxdIMER9yjUkUMY@G3pkAm7SbIjUL0buxGZUbgDVt5UPA51kobqyCxVdleOejcYSc/iUg5Li1dhbnoAQ7zBJoORiNaCYoT@FcGek1PU6@NX@5CkUXlXI9HMapuq3kTmIM2Vkc/EGE6obPOcumXq9welPNHysUoG8Kr23jFeH0brxmnmVBWRCjxiIoSodVOqSfUHBoOw3RyOgVHseIwCiZNn0npAwblTPOgW5npL1md0RYY6m4JJAmHg24R2RvbMRUWDI217g9HU65HqfSamryIs4eRzf21h7RrcMxlBOgSVNdhxr3YNPJZ@UBX/Wtq9ji4hufmr7ioTVNMxwJ3VITVcbp9KQXXjciLBWoRsyl99oecIfcu57L1mUX6tsJFAtXtJ9i7fJd7dQzseIEPYi0GorkwvhMM/xGsW@/NVfXfM/WaHw#singeli
i didnt find info on how to use this for verification.
c allows a wide range of fp behaviors that similar looking
code may not capture.
e.g. the correctness of the FLT_EVAL_METHOD==2 case is not
obvious, nor if the e==0x7ff check is needed given that
branch is never taken on most implementations, would the
tool catch that if you removed this check?.
that said, tools that can verify numerical results over a
large input space are useful.. if we know what was verified.
>
> Thanks to https://github.com/dzaima for doing this.
Powered by blists - more mailing lists
Confused about mailing lists and their use?
Read about mailing lists on Wikipedia
and check out these
guidelines on proper formatting of your messages.
