feat(BV, CP): Add bitlist propagators for add/sub

[bclement-ocp]

This patch adds propagators on the bitlist domain for addition and
subtraction. These propagators are able to compute low bits
independently of high bits; in particular, we now know that the sum of
two even (or two odd) numbers is even.

If there is a bit pattern that prevents carry propagation (e.g. two [0]s
for addition), we are also able to compute the following bits precisely.

Note that we do not currently decompose addition/subtraction according
to these propagators -- for instance, we do not know that
(bvadd (concat x #b0) (concat y #b0)) is (concat (bvadd x y) #b0).

Note: depends on #1058, #1083, #1084, #1085, and #1144. Only the latest commit with title "feat(CP): Add bitlist propagators for add/sub" is included in this PR.

[Halbaroth]

I read carefully your comments and the proofs seem okay but my concern about these comments is that I have no intuition at all after reading the proof. I basically checked them step by step. I believe we can do better and actually I found a simpler but a bit more abstract proof.

I keep your definition of carry position. I also extract your first lemma but I suggest an alternative proof:

Lemma A: for all bitvectors x and y, flipping bits from 0 to 1 in x or y does not erase carry positions in the sum x+y.

Proof: We proceed by induction on the carry position i. If i = 0, we have x_0 = y_0 = 1 and clearly switching a bit from 0 to 1 cannot remove this carry position. Let us assume we have prove the statement for any carry position < i. If x_i = y_i = 1, we proceed as before. Otherwise, we have x_i = 1 or y_i = 1 and i-1 is a carry position. By induction we know that switching a bit from 0 to 1 cannot remove the carry position i-1 and we still have x_i = 1 or y_i = 1 after this transformation. So i is still a carry position.

Now, we state the main result:

Lemma: for all bitlists a and b, we denote by a+b the set { x + y | x in a, y in b }. Then a+b is a bitlist and the position i is known for a+b if and only if i is known in a, b and the bitvectors a.bits_set + b.bits_set and a.bits_set + a.bits_unk + b.bits_set + b.bits_unk agrees at i.

Before proving this lemma, let us introduce few notations. For bitvectors x and y in a bitlist a, we write x ⇝a y if y is obtained from x by flipping one unknown bit in a from 0 to 1. For a bitlist a, we write m_a = a.bits_set and M_a = a.bits_set + a.bits_unk.

Now, remark that any value x of a is the end of a sequence m_a ⇝a ... ⇝a x and M_a is maximal in this process. So any value x+y of a+b is obtained by a sequence (m_a, m_b) ⇝ .... ⇝ (x, y) (where (u, v) ⇝ (w, z) means u ⇝a w and v ⇝b z) and M_a + M_b is maximal in this process.

Let us prove the equivalence:

• If m_a + m_b and M_a + M_b does not agree at i, i cannot be a known bit of a+b as m_a + m_b and M_a + M_b are in a+b.
• If i is known in a and b and m_a + m_b and M_a + M_b agrees at i and the bit is w, consider x in a and y in b. We show that x+y at i is w. The case i = 0 is easy because there is no carry involved. Assume that i > 0.
  Now, we prove that i-1 is a carry position of x+y if and only if i-1 is a carry position of m_a + m_b. By repeat lemma A, if i-1 is a carry position of x+y then i-1 is a carry position of M_a + M_b. But if i-1 is not a carry position of m_a + m_b then m_a + m_b and M_a + M_b cannot agree at i (because i is known in a and b). If i-1 is not a carry position of x+y then again by apply lemma A, i-1 is not a carry position of m_a + m_b. So the value of x+y at i is w.

[Halbaroth]

I thought that bits_unk is the set of unknown bits? Do you mean that i is not active in a.bits_unk?

[bclement-ocp]

Yes, I meant that it is cleared in both. Will fix.

[Halbaroth]

We should start this comment by explaining what we are proving, otherwise we have to read all the comment before discovering that it is a proof of correction.

[Halbaroth]

It is confusing to use x here because x denotes a completely different thing in the comment above.

[Halbaroth]

Same remark.

[bclement-ocp]

@Halbaroth Rewrote the proof taking in consideration your remarks. I tried to avoid induction since I don't think it is necessary here if we think about integers. Let me know if this is better.

[Halbaroth]

Thanks :)
Please don't merge before I finish #1169