[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <CABaUXi5Wk6gXR26imsOPc1udbxvn+P7ZaBa_yxv9ZrmOupShtA@mail.gmail.com>
Date: Thu, 3 Sep 2026 09:32:19 +0100
From: Sergey Davidoff <shnatsel@...il.com>
To: Rich Felker <dalias@...c.org>
Cc: musl@...ts.openwall.com
Subject: Re: [PATCH v4 2/2] math: fmaf rewrite
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.
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
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.
