Prove that the next multiple of 4 is obtained using the next formula

I was reading an assembly procedure that needed to align addresses on 4 bytes boundary for performance reasons so it has used the next statement that i formulated as a theorem to be proven.

Let $$s$$ be an integer that is not a multiple of 4 ($$s \% 4 \neq 0$$). $$m$$, the first next multiple of 4 such that $$m \gt s$$ is obtained using the following formula, where the operands are expressed in base 2 (Binary): $$m = s + (\lnot s \land 11)$$ ($$\lnot a$$ will return the 2's complement of $$a$$).

How to prove that ?

• @dkaeae Yes. I made a mistake i forgot to tell that the negation $\lnot$ will actually return the 2's complement of its operand (The Intel's x86 neg instruction). Mar 15 '19 at 17:05
• Yes, but it still doesn't work. Now if $s = 1$, then $m = 3$. Mar 15 '19 at 17:07
• In fact, $\text{and}(a, 3)$ yields a number strictly smaller than $4$ for any $a$. Mar 15 '19 at 17:08
• @dkaeae Damn man, i feel too dumb. That is actually the distance that is needed to reach the next multiple of 4. God, sorry for this spaghetti i made. I just corrected the formula, take a look. Mar 15 '19 at 17:43

Suppose that $$s = 4a+b$$, where $$0 \leq b < 4$$; by assumption, $$b \neq 0$$. If the numbers are $$n$$ bit long, then $$\lnot s = 2^n - s = 4(2^{n-2}-a) + (4-b)$$. Since $$b \neq 0$$, the last two bits of $$\lnot s$$ will be $$4-b \in \{1,2,3\}$$. Therefore $$(\lnot s) \land (11)_2 = 4-b$$. Adding this to $$s$$, we get $$4a+b+4-b = 4(a+1)$$.
• Oh great, that's so beautifully done. I really missed the idea that $\lnot s = 2^n - s$ . That was the key for proving it. Thanks professor. The thing that puzzles me is how did the programmer knew about such a fact ?! Is it something that could be intuitively figured out and later be proved ? for example, the fact that $and(n, 3)$ always gives you the distance to the previous multiple of 4 is easy to notice and then prove. But this one is really tricky. What do you think professor @Yuval Filmus, is it a known technique for the people that work on assembly level ? Mar 15 '19 at 22:55