Comment by ryao

They are sometimes very good at using mathematical identities to do simplifications. The following commit was actually inspired by the output of GCC:

https://github.com/openzfs/spl/commit/8fc851b7b5315c9cae9255...

Jason had noticed that GCC’s assembly output did not match the original macro when looking for a solution to the unsigned integer overflow warning that a PaX GCC plugin had output (erroneously in my opinion). He had conjectured we could safely adopt GCC’s version as a workaround. I gave him the proof of correctness for the commit message and it was accepted into ZFS. As you can see from the proof, deriving that from the original required 4 steps. I assume that GCC had gone through a similar process to derive its output.