Proofs: Roaring bitmap

Each Roaring bitmap operation keeps the invariant and returns the right result full

This proof shows: correctness.

Setting. For $0 \le x < 2^{32}$ write $h(x) = \lfloor x / 2^{16} \rfloor$ and $\ell(x) = x \bmod 2^{16}$, so $x = 2^{16} h(x) + \ell(x)$ with $0 \le h(x), \ell(x) < 2^{16}$, and the map $x \mapsto (h(x), \ell(x))$ is a bijection onto pairs of 16-bit integers. A container $C$ stands for a set $V(C) \subseteq \{0, \ldots, 2^{16} - 1\}$: the values of an array container, or the positions $\ell$ such that bit $\ell \bmod 64$ of word $\lfloor \ell / 64 \rfloor$ is 1 for a bitmap container. A Roaring bitmap $R$ with keys $k_0, \ldots, k_{m-1}$ and containers $C_0, \ldots, C_{m-1}$ stands for

The invariant is: (I1) $k_0 < k_1 < \cdots < k_{m-1} < 2^{16}$; (I2) $V(C_i) \neq \emptyset$ for each $i$; (I3) an array container is strictly increasing with values below $2^{16}$ and has at most 4096 values; (I4) a bitmap container has 1024 words, a stored count equal to the number of ones, and that count is above 4096.

Lemma 1 (chunks). Under (I1), for each key $k$ the set $\{\ell : 2^{16} k + \ell \in \operatorname{set}(R)\}$ is $V(C_i)$ when $k = k_i$, and empty when $k$ is not a key.

Proof. By the bijection, $2^{16} k_i + \ell = 2^{16} k + \ell'$ with $\ell, \ell' < 2^{16}$ holds only when $k_i = k$ and $\ell = \ell'$. By (I1) at most one index $i$ has $k_i = k$. $\square$

Lemma 2 (conversions). Converting an array container to a bitmap container, or a bitmap container to an array container, does not change $V$. After the conversion at line L6, done when an array has more than 4096 values, (I4) holds; after the conversion at line L12, done when a bitmap has at most 4096 ones, (I3) holds as long as the bitmap is nonempty.

Proof. The array to bitmap conversion sets exactly the bits at the positions in the array and counts them, so the count is the number of values, above 4096. The bitmap to array conversion lists the set positions in increasing order, which gives a strictly increasing array of the same values, of length equal to the count, at most 4096. $\square$

CONTAINS. Line L8 finds by binary search, which is correct because the keys are sorted by (I1), the index $i$ with $k_i = h(x)$ if it exists. If it does not, Lemma 1 says no member has high part $h(x)$, so $x \notin \operatorname{set}(R)$ and false is right. Otherwise line L9 tests $\ell(x) \in V(C_i)$, by binary search in a sorted array (I3) or by reading one bit, and by Lemma 1 this holds exactly when $x \in \operatorname{set}(R)$.

ADD. Let $R'$ be the result. If $h(x)$ is not a key, line L2 inserts it at the position found by binary search, which keeps the keys strictly increasing, with an empty array container. Then line L5 inserts $\ell(x)$ in sorted order if it is absent, so the array stays strictly increasing, or line L7 sets bit $\ell(x)$ and adds 1 to the count exactly when the bit was 0, so the count stays equal to the number of ones. In both cases the container of $h(x)$ now stands for its old set together with $\ell(x)$, which is nonempty, so (I2) holds again for the new key. If the array grew to 4097 values, line L6 converts it, and by Lemma 2 the set is the same and (I4) holds. A bitmap only grows, so its count stays above 4096. No other container changes. By Lemma 1, $\operatorname{set}(R') = \operatorname{set}(R) \cup \{x\}$.

REMOVE. If $h(x)$ is not a key, line L10 returns, and $x \notin \operatorname{set}(R)$ by Lemma 1, so nothing must change. Otherwise line L11 takes $\ell(x)$ out of $V(C_i)$ if it is there: deletion from a sorted array keeps it sorted, and clearing a bit subtracts 1 from the count exactly when the bit was 1. An array only shrinks, so it still has at most 4096 values. A bitmap whose count falls to 4096 is converted at line L12, and by Lemma 2 its set is the same and (I3) holds. If the container is now empty, line L13 deletes it and its key; deleting an entry from a strictly increasing array keeps it strictly increasing, so (I1) and (I2) hold. The other containers do not change, so $\operatorname{set}(R') = \operatorname{set}(R) \setminus \{x\}$.

UNION and INTERSECTION. The merge loop U2 to U6 keeps two indices $i$ and $j$ and appends keys to $T$. At each step it appends the smaller of $R.\mathrm{keys}[i]$ and $S.\mathrm{keys}[j]$, or the common value once when they are equal, and then advances past it. Since both key arrays are strictly increasing by (I1), every key appended is larger than all earlier ones, so the keys of $T$ are strictly increasing, and each key of either input is visited exactly once. For a key $k$, Lemma 1 gives the chunk of $\operatorname{set}(R) \cup \operatorname{set}(S)$ as $V_R(k) \cup V_S(k)$, where $V_R(k)$ is empty when $k$ is not a key of $R$. If $k$ is a key of only one input, the union copies that container, whose set is the chunk, and the intersection appends nothing, which is right because the other chunk is empty. If $k$ is a key of both, OR-CONTAINERS returns a container for $V_R(k) \cup V_S(k)$: a merge of two sorted arrays gives the sorted union, and a word-by-word OR gives a bitmap of the union with a fresh count; the result is converted to the layout that its size requires, which by Lemma 2 does not change its set and gives (I3) or (I4). The union of two nonempty sets is nonempty, so (I2) holds. For the intersection, the AND of the two containers gives $V_R(k) \cap V_S(k)$ by the same argument, and the result is appended only when it is nonempty, so (I2) holds. By Lemma 1 for $T$, $\operatorname{set}(T)$ is the union, or the intersection, of the two sets.

Conclusion. Every operation starts from a structure that satisfies (I1) to (I4), ends with one that satisfies them, and gives the result of the abstract operation on $\operatorname{set}(R)$. The empty bitmap, with no keys, satisfies the invariant and stands for $\emptyset$, so by induction on the number of operations every reachable Roaring bitmap is valid and every answer is correct. $\blacksquare$