See also this [1] blog post on the complementary operation -- propagating arithmetic bounds through bitwise arithmetic -- and my own post [2] on getting a tighter bound on propagating bitwise bounds if you also know arithmetic bounds.
This was a very interesting read! I will try finding an algebraic proof of the addition function in my time.
The author mentions that this is frequently used in optimizing compilers and program analysis but does not elaborate on this statement. Can someone provide more context?
Author here - I believe this 2020 post resurfaced as known-bits optimisation was recently added to PyPy (Python implementation using a JIT compiler), which this thread discusses:
It includes discussion of where this kind of optimisation helps (not most "normal" Python code, but some code like emulators with lots of bitwise operations is ~30% faster), links to LLVM and Linux kernel implementations, and some related blog posts and papers. (I believe the Linux eBPF people came up with all of the ideas here before I did, though I wasn't aware of it at the time - it's easy to forget the Linux kernel has an optimising compiler in it.)
I'm not sure if that's what you mean by context - happy to answer questions.
There’s an example in the linked thread. Suppose you write some code like
if (a+b) % 2 == 0:
…
And the compiler is able to figure out that a and b are even (that is they both have 0 in the lsb), or if it figures out that a = b, this kind of known-bits tracking allows it to get rid of the branch. The code in the OP can be used to make tracking known-bits fast enough to be practical
To try to make it more "concrete", compilers tend to end up processing an absurd mess of code, that does things that superficially look silly, due to extensive inlining.
The code above is entirely plausible for C code checking the alignment of a total size, where "a" and "b" are the sizes of two parts, both calculated by a multiplication that ensures their evenness.
Another realistic examples are flags-fields, where each bit represents a boolean. For example, the compiler should be able to optimise:
flags |= 0x100;
if (!(flags & 0x100)) { ... }
Addition might factor in either as a substitution for bitwise-OR or bitwise-XOR where the author has prior knowledge that the two are equivalent (and assumes it will lead to better code generation), as part of SWAR (simd-within-a-word) code, or in cases where integer fields are packed alongside flags (e.g. a refcount and a couple of flags, or a string-length and some flags).
If this seems rare and unusual, that's cool – in general it is. But these strategies are very heavily used in performance-critical code, where using multiple variables would cause a measurable slowdown, so it makes sense that compilers care about optimising this kind of thing.
[1] http://bitmath.blogspot.com/2023/07/propagating-bounds-throu...
[2] https://news.ycombinator.com/item?id=36967219