Proofs: XOR linked list

The XOR linked list keeps its invariant and returns the right keys full

This proof shows: correctness.

Claim. Assume the invariant (X) before an operation. Then each of PUSH-FRONT, POP-FRONT (on a list that is not empty), REVERSE, PUSH-BACK, POP-BACK and INSERT-BETWEEN (on two adjacent nodes $p$ before $q$) leaves a list that satisfies (X) and holds the right sequence of keys; the two pops return the key that the deque asks for; and TRAVERSE visits the keys from the front to the back and stops.

Setup. The list holds the nodes $x_1, \dots, x_n$ in order, with keys $k_1, \dots, k_n$, and $x_0 = x_{n+1} = 0$. No node has address 0, and distinct nodes have distinct addresses. The invariant is

(X) $x_i.np = x_{i-1} \oplus x_{i+1}$ for $1 \le i \le n$; $L.head = x_1$ and $L.tail = x_n$ when $n \ge 1$; $L.head = L.tail = 0$ when $n = 0$.

We use that $\oplus$ is associative and commutative, $a \oplus 0 = a$ and $a \oplus a = 0$. Hence $(a \oplus b) \oplus b = a$ (cancellation). To prove (X) for a new sequence $y_1, \dots, y_{n'}$ it is enough to check the link of each node whose predecessor or successor differs from before, since the link of every other node is not written and its neighbours are the same.

Lemma 1 (PUSH-FRONT). The new sequence is $y = (x, x_1, \dots, x_n)$, where $x$ is the new node, with key $k$. Line L1 gives $x$ an address that is not 0 and not in use. Line L2 sets $x.np = L.head$. If $n = 0$, then $L.head = 0$, so $x.np = 0 = 0 \oplus 0$, which is (X) for the one node $x$; line L4 sets $L.tail = x$ and line L5 sets $L.head = x$. If $n \ge 1$, then $x.np = x_1 = 0 \oplus x_1$, as (X) asks for $y_1 = x$. The node $x_1$ now has predecessor $x$ instead of 0. Line L3 sets $x_1.np = (0 \oplus x_2) \oplus x = x \oplus x_2$, as (X) asks for $y_2 = x_1$. No other node has a new neighbour. Line L5 sets $L.head = x$, and $L.tail = x_n$ is still the last node. $\square$

Lemma 2 (POP-FRONT). Here $n \ge 1$, and the new sequence is $(x_2, \dots, x_n)$. Line L6 sets $x = x_1$ and, by (X), $nxt = x_1.np = 0 \oplus x_2 = x_2$. If $n = 1$, then $nxt = 0$, line L8 sets $L.tail = 0$ and line L9 sets $L.head = 0$, which is (X) for the empty list. If $n \ge 2$, the node $x_2$ now has predecessor 0 instead of $x_1$, and line L7 sets $x_2.np = (x_1 \oplus x_3) \oplus x_1 = x_3 = 0 \oplus x_3$, as (X) asks. Line L9 sets $L.head = x_2$, and the tail is unchanged. No other node has a new neighbour. Line L10 returns $k_1$, the front key, and frees $x_1$, which is no longer in the list. $\square$

Lemma 3 (TRAVERSE). We show by induction on $i$ that at the $i$-th test of line L12, for $1 \le i \le n + 1$, $prev = x_{i-1}$ and $cur = x_i$. For $i = 1$, line L11 sets $prev = 0 = x_0$ and $cur = L.head = x_1$ (which is 0 when $n = 0$). Assume the statement for some $i \le n$. Then $cur = x_i \ne 0$, so the body runs, line L13 visits $k_i$, and line L14 sets $nxt = x_i.np \oplus x_{i-1} = (x_{i-1} \oplus x_{i+1}) \oplus x_{i-1} = x_{i+1}$ by (X) and cancellation. Line L15 sets $prev = x_i$ and $cur = x_{i+1}$, which is the statement for $i + 1$. So the loop visits $k_1, \dots, k_n$ in this order. At the test number $n + 1$, $cur = x_{n+1} = 0$ and the loop stops; it cannot stop earlier because $x_i \ne 0$ for $i \le n$. $\square$

Lemma 4 (REVERSE, PUSH-BACK, POP-BACK). Let $y_i = x_{n+1-i}$, so $y_0 = x_{n+1} = 0$ and $y_{n+1} = x_0 = 0$. For $1 \le i \le n$, $y_i.np = x_{n+1-i}.np = x_{n-i} \oplus x_{n+2-i} = y_{i+1} \oplus y_{i-1} = y_{i-1} \oplus y_{i+1}$ by commutativity. After line R1, $L.head = x_n = y_1$ and $L.tail = x_1 = y_n$ (both 0 when $n = 0$). So the list satisfies (X) for the reversed sequence: REVERSE reverses the list. PUSH-BACK reverses, inserts $k$ at the front by Lemma 1, and reverses again; the result is the sequence $x_1, \dots, x_n$ followed by the new node, and it satisfies (X) by Lemmas 1 and 4. POP-BACK reverses, removes and returns the front key of the reversed list by Lemma 2, which is $k_n$, and reverses again; the result is $x_1, \dots, x_{n-1}$ and satisfies (X). $\square$

Lemma 5 (INSERT-BETWEEN). Let $p = x_j$ and $q = x_{j+1}$ with $1 \le j < n$. The new sequence is $(x_1, \dots, x_j, x, x_{j+1}, \dots, x_n)$. Line B2 sets $x.np = x_j \oplus x_{j+1}$, which is (X) for $x$. The node $x_j$ has the new successor $x$ instead of $x_{j+1}$; line B3 sets $x_j.np = (x_{j-1} \oplus x_{j+1}) \oplus x_{j+1} \oplus x = x_{j-1} \oplus x$. The node $x_{j+1}$ has the new predecessor $x$ instead of $x_j$; line B4 sets $x_{j+1}.np = (x_j \oplus x_{j+2}) \oplus x_j \oplus x = x \oplus x_{j+2}$. No other node has a new neighbour, and $p$ and $q$ are not the ends of the new list, so head and tail stay right. $\square$

Conclusion. The empty list ($L.head = L.tail = 0$, no node) satisfies (X). By Lemmas 1, 2, 4 and 5, each update keeps (X) and changes the key sequence as the deque operations require, and by Lemmas 2 and 4 each pop returns the key at its end. By Lemma 3, TRAVERSE reads the keys in order. By induction on the number of operations, every sequence of operations from the empty list gives the same results as an abstract deque. $\blacksquare$