# Christopher Meiklejohn

home lasp research courses publications videos code curriculum vitae

## Distributed data structures with Coq: PN-Counters

20 Jun 2013

Continuing my previous post on proving properties about CRDTs, specifically G-Counters, we’ll now look at the PN-Counter, a counter which allows the value to both increment and decrement while guaranteeing convergence. Since this builds off of the lemmas proven in the previous post, I highly recommend you read that post first.

First, let’s define a PN-Counter as a product of two G-Counters. We’ll use one set for counting the increments, and one for counting the decrements.

Then, let’s define increment and decrement functions for a particular actor, which call the G-Counter increment function on each set. In this example, we use fst and snd to destructure the PN-Counter into two seperate counters, and then after we perform the increment we use pair, the product constructor, to rebuild the PN-Counter.

Let’s define a function to reveal the current value of the PN-Counter, by subtracting the values of each counter.

Then, let’s define merge, comparsion, and equality functions, which leverage the functions we’ve defined over G-Counters.

Cool. Now, let’s start proving things.

First, let’s prove that the merge operation commutes. Similar to our G-Counter proof, we can simply perform the necessary destructuring of the PN-Counter type, and then apply the lemma we’ve previously defined which shows that the merge operation on clocks commute.

Same thing, we can use the existing lemmas we’ve proven about G-Counter’s and their merge operation, and apply it to prove that, in addition to being commutative, they are also associative and idempotent.

Now, let’s prove that both the increment and decrement operations monotonically advance the structure. This is extremely trivial, as we’ve already proven that incrementing an individual G-Counter monotonically advances the structure, given that the increment and decrement are both only increment operations operating on either side of a product.

Now, let’s confirm that the merge operation of the PN-Counter cause the data structure to monotonically advance. This proof is trivial, given we’ve already proven that this property holds true for the G-Counter. We can simply apply the theorem we’ve already defined.

Qed.

View this story on Hacker News.