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

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/8fc851b7b5315c9cae92557be6c32e1ee236201f 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.