[<prev] [next>] [thread-next>] [day] [month] [year] [list]
Message-ID: <c3a94a37-03c9-49ec-b8f9-334926312d66@gmail.com>
Date: Fri, 4 Sep 2026 19:31:30 +0300
From: dzaima <dzaimagit@...il.com>
To: Szabolcs Nagy <nsz@...t70.net>
Cc: musl@...ts.openwall.com
Subject: Re: [PATCH v4 2/2] math: fmaf rewrite
Hello from the person that did the SMT verification :)
On 9/3/26 15:32, Szabolcs Nagy wrote:
> note the code is not correct under some fast-math flags.
Wanting an exact FMA implementation under any fast-math flags doesn't
exactly make much sense in the first place, of course.
My SMT code assumes IEEE-754 to be exactly followed (no FTZ/DAZ), and for
there to be no implicit contraction. (replacing xy+z with an explicit FMA
still passes, so at least that bit of contraction would be fine, albeit
funny).
I've modeled NaN bit pattern propagation rules following LLVM's descriptions
(https://llvm.org/docs/LangRef.html#behavior-of-floating-point-nan-values),
with 3 different models: x86 (which is identical to ARM and RISC-V),
SPARC, and wasm. I'd assume GCC's behaviors should be similar, but haven't
happened across any docs for it.
> i didnt find info on how to use this for verification.
The SMT interface is not public yet, sorry... So the code samples are
"useless" other than as a reference to how I translated the code.
> 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?.
Cannot comment on FLT_EVAL_METHOD==2; that's a massive mess. Bitwuzla
theoretically could do IEEE-754 binary128, but other float formats (incl.
x87's) are experimental. Never mind the problem of how exactly compilers
handle it. (and larger floats would probably take much more time to verify
anyway (for reference, the current version takes 14 to 25 minutes
(single-threaded) on my old PC to verify)).
Removing the e==0x7ff check does still verify as correct for all the
aforementioned NaN propagation rules. (all checks in this email are done
with the e==0x7ff check removed)
There do exist rules where the check is needed to maintain strict
correctness; e.g. with the x86 rule, except 64-bit float ops are allowed
to optionally change QNaN payload to 0x4000000000000 (i.e. with top
payload bit (after quiet bit) set; no such change for 32-bit floats
though!), my tool spits out this counterexample for the version without a
e==0x7ff check:
https://dzaima.github.io/paste/#0hVbNjts2EL77KSYJ0LUSb6EfW/7prtGiyB4DFL2HkL2kLURLbSlqa6@...Oe@...uDxJZ4aSbK1drw62hsPv4zdDzlDKF4VZC51oVeove/j@...QgbAbKx7KIjs40gJ0biEBI1Wq5YPUdjEAePLFDm7hw/e//yUrEHuy/B99skLxjNbvn5JPMPR307tffHwCD102MRvJBADIZPbuFTFRxwfv2FqoeIwjKssTK9a5fpLGVjg24rXrFjfuViYcWhdwqLLDTVjjb43Gu7u7X0lk6LvHIzKccoEMg@...j7VzD96mCpuiARmN6sovBGL7RimojRn9PRIaE7Hk9zfV0/xiFV2LDNRpug9xROcnIuS4Uam2krzaKStSo6GuDuaOXMc430kJI55Q1BsjUi1qZh0BG8mITk6gsAX8pRj6jjI2dBgGBrDmCND6I@...7glKGJJAj6@...FM@...x5Dzyh2CaZ@...c6KSrJBM0Y0uyoCZ5B8VEpOSeDaOJuNJ3KeJevCohWWy4ogQOJu/iIAkWlM6xLhFbI4Q03EfMRE21X2hbqgFc7xBRIe5g9nki2wAj4ndIipVMDwK0YNNbvMq82uQNIstgYjMbk1ebrYicFz9scUr/E7Z6@...fKwK/ygXzwfD@...KqJwtPyi8IXBxaPcWl0cZbF@...Mc0u8tKs5dn@...i2hQPq4gaEUKoh6TC3pNwJ1lxC1j/n4RjilZCVA/egd1KSFb5k4S3jZi32GP1lWVPrrM9POZFka4yicCizOwIVqXFJqzRrXjWiwkFJEayY5Va2iIsbQ2HNKArcfSu/bZiByinTYjSgPdBZcpM1sNkwTleub81/XmYgZ/JWwzp14MKA3cpwXxgMjAT9WBwL1Ehrl6tR4DCVY0wmmlggduIL3Ry1h5Qr7M/kQNRuHZ77zQCdm7lvft7dgIW4DbiRMaFq4LviQtXAjfgC12eWysFtaOi3MF72ONAyeHg0Ad4JjMlE@...9fSoC3JHJbpcjlB2T/gTkwVxd62IedlR6Dcg@...hc0TY5uSuoDNFPCDbkipa6DMCY@...2Q@...6SVrul2CWwTfG27Aq0GhyNanSkmrCSKkwukVbdcQhx58AYXIjU0zBtbkNIhxn4Dz96IknBN@...YLba9x3nlURZZmglIO/1LTya/CG30t08BXzGWTe@...z/rqF4BXBinOddqrPx4RHy8rCisOXS0Vn/Aq/bW754@...h1O3vFw/R8#singeli
> that said, tools that can verify numerical results over a
> large input space are useful.. if we know what was verified.
This is just generally what SMT does well; Bitwuzla in particular,
especially at float stuff, in my experience, is much faster than Z3 & CVC5.
My tool is just a dumb mapping of code in the single
configurable-enough programming language I know of, to SMT.
The SMT task done here is to try to find a configuration of argument bit
patterns for which there exists a result bit pattern that the custom impl
(tgt_musl) can produce, which SMT-LIB's native FMA op (or custom NaN bit
patterns as per NaN propagation rules, if applicable) cannot. i.e. if the
code is a refinement of FMA.
The originally-used rounding mode was the regular nearest-ties-to-even.
I've now ran it through all 5 rounding modes though, which all passed.
There's no attempt at any verification of float exception/flag values, in
case that's an aspect that matters; SMT-LIB doesn't come with any ops for
it, and I don't trust myself on implementing them correctly myself (not
that I would even care to for my purposes).
anyway, that's enough rambling about my little tool that I only really
wanted to sanity-check a new algorithm with :) (I hope this email gets to
roughly the correct place, I don't do emails)
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.
